|
|
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. 33-41.
|
|
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
|
|
|
|