The OEIS is supported by the many generous donors to the OEIS Foundation.

 Hints (Greetings from The On-Line Encyclopedia of Integer Sequences!)
 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 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)} A369410(n,k). 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 Cf. A024495, A368946, A369173, A369409, A369410, A369413. Sequence in context: A160249 A173800 A175174 * A136137 A287895 A050223 Adjacent sequences: A369409 A369410 A369411 * A369413 A369414 A369415 KEYWORD nonn,hard,more AUTHOR Paolo Xausa, Jan 23 2024 STATUS approved

Lookup | Welcome | Wiki | Register | Music | Plot 2 | Demos | Index | Browse | More | WebCam
Contribute new seq. or comment | Format | Style Sheet | Transforms | Superseeker | Recents
The OEIS Community | Maintained by The OEIS Foundation Inc.

Last modified August 11 16:53 EDT 2024. Contains 375073 sequences. (Running on oeis4.)