

A369412


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


2



1, 4, 13, 11, 18, 16, 25, 23, 24, 22, 26, 24, 34, 32, 33, 31, 35, 33, 34, 32, 39, 37, 49
(list;
graph;
refs;
listen;
history;
text;
internal format)



OFFSET

2,2


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


LINKS



FORMULA



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


CROSSREFS



KEYWORD

nonn,hard,more


AUTHOR



STATUS

approved



