%I #9 Jan 25 2024 08:05:10
%S 2,13,94,75,165,139,308,269,348,299,482,423,647,581,780,701,893,807,
%T 1064,965,1281,1175,1654
%N Maximum number of symbols of a "normal" proof (see comments) for strings (theorems) in the MIU formal system that are n characters long.
%C See A368946 for the description of the MIU formal system, A369411 for the triangle of the corresponding symbol lengths and A369409 for the definition of "normal" proof.
%D Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41.
%H Armando B. Matos and Luis Filipe Antunes, <a href="https://www.researchgate.net/publication/2845974_Short_proofs_for_MIU_theorems">Short Proofs for MIU theorems</a>, Technical Report Series DCC-98-01, University of Porto, 1998.
%H Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%F a(n) = max_{k=1..A024495(n)} A369411(n,k).
%t MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
%t MIUProofSymbolCount[t_] := Module[{c = Length[t], nu = Count[t,0], ni}, ni = 2*nu+c; c += nu(nu+c+2); While[ni > 1, If[OddQ[ni], c += (7*ni+3)/2 + 13; ni = (ni+3)/2, c += ni/2 + 1; ni/=2]]; c+1];
%t Map[Max, Map[MIUProofSymbolCount, Array[MIUDigitsW3, 15, 2], {2}]]
%Y Cf. A024495, A368946, A369173, A369409, A369411, A369412.
%K nonn,hard,more
%O 2,1
%A _Paolo Xausa_, Jan 23 2024