This is a front-end for the Online Encyclopedia of Integer Sequences, made by Christian Perfect. The idea is to provide OEIS entries in non-ancient HTML, and then to think about how they're presented visually. The source code is on GitHub.
%I A369412 #10 Jan 25 2024 08:05:02
%S A369412 1,4,13,11,18,16,25,23,24,22,26,24,34,32,33,31,35,33,34,32,39,37,49
%N A369412 Maximum length of a "normal" proof (see comments) for strings (theorems) in the MIU formal system that are n characters long.
%C A369412 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.
%D A369412 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41.
%H A369412 Armando B. Matos and Luis Filipe Antunes, <a href="https://www.researchgate.net/publication/2845974_Short_proofs_for_MIU_theorems">Short Proofs for MIU theorems</a>, Technical Report Series DCC-98-01, University of Porto, 1998.
%H A369412 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369412 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%F A369412 a(n) = max_{k=1..A024495(n)} A369410(n,k).
%t A369412 MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
%t A369412 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];
%t A369412 Map[Max, Map[MIUProofLineCount, Array[MIUDigitsW3, 15, 2], {2}]]
%Y A369412 Cf. A024495, A368946, A369173, A369409, A369410, A369413.
%K A369412 nonn,hard,more
%O A369412 2,2
%A A369412 _Paolo Xausa_, Jan 23 2024