login
A369413
Maximum number of symbols of a "normal" proof (see comments) for strings (theorems) in the MIU formal system that are n characters long.
2
2, 13, 94, 75, 165, 139, 308, 269, 348, 299, 482, 423, 647, 581, 780, 701, 893, 807, 1064, 965, 1281, 1175, 1654
OFFSET
2,1
COMMENTS
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.
REFERENCES
Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41.
LINKS
Armando B. Matos and Luis Filipe Antunes, Short Proofs for MIU theorems, Technical Report Series DCC-98-01, University of Porto, 1998.
Wikipedia, MU Puzzle.
FORMULA
a(n) = max_{k=1..A024495(n)} A369411(n,k).
MATHEMATICA
MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
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];
Map[Max, Map[MIUProofSymbolCount, Array[MIUDigitsW3, 15, 2], {2}]]
CROSSREFS
KEYWORD
nonn,hard,more
AUTHOR
Paolo Xausa, Jan 23 2024
STATUS
approved