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,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

Table of n, a(n) for n=2..24.

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".

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

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

Sequence in context: A300764 A209470 A140636 * A282724 A104255 A369202

Adjacent sequences: A369410 A369411 A369412 * A369414 A369415 A369416

Keyword

nonn,hard,more

Author

Paolo Xausa, Jan 23 2024

Status

approved