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, 13, 94, 75, 165, 139, 308, 269, 348, 299, 482, 423, 647, 581, 780, 701, 893, 807, 1064, 965, 1281, 1175, 1654

Offset: 2

Author

Paolo Xausa, Jan 23 2024

Keywords

• nonn
• hard
• more

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.
• Index entries for sequences from "Goedel, Escher, Bach".

Crossrefs

Cf. A024495, A368946, A369173, A369409, A369411, A369412.

Programs

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}]]

Formula

a(n) = max_{k=1..A024495(n)} A369411(n,k).