A369412 Maximum length of a "normal" proof (see comments) for strings (theorems) in the MIU formal system that are n characters long.

1, 4, 13, 11, 18, 16, 25, 23, 24, 22, 26, 24, 34, 32, 33, 31, 35, 33, 34, 32, 39, 37, 49

Offset: 2

Author

Paolo Xausa, Jan 23 2024

Keywords

• nonn
• hard
• more

Comments

See A368946 for the description of the MIU formal system, A369410 for the triangle of the corresponding proof 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, A369410, A369413.

Programs

Mathematica

MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
MIUProofLineCount[t_] := Module[{c = Count[t, 0], ni}, ni = Length[t] + 2*c; While[ni > 1, If[OddQ[ni], ni = (ni+3)/2; c += 4, ni/=2; c++]]; c+1];
Map[Max, Map[MIUProofLineCount, Array[MIUDigitsW3, 15, 2], {2}]]

Formula

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