cp's OEIS Frontend

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

%I A369413 #9 Jan 25 2024 08:05:10
%S A369413 2,13,94,75,165,139,308,269,348,299,482,423,647,581,780,701,893,807,
%T A369413 1064,965,1281,1175,1654
%N A369413 Maximum number of symbols of a "normal" proof (see comments) for strings (theorems) in the MIU formal system that are n characters long.
%C A369413 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.
%D A369413 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41.
%H A369413 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 A369413 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369413 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%F A369413 a(n) = max_{k=1..A024495(n)} A369411(n,k).
%t A369413 MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
%t A369413 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];
%t A369413 Map[Max, Map[MIUProofSymbolCount, Array[MIUDigitsW3, 15, 2], {2}]]
%Y A369413 Cf. A024495, A368946, A369173, A369409, A369411, A369412.
%K A369413 nonn,hard,more
%O A369413 2,1
%A A369413 _Paolo Xausa_, Jan 23 2024