cp's OEIS Frontend

A369410 Irregular triangle read by rows: row n lists the length of a "normal" proof (see comments) for each of the distinct derivable strings (theorems) in the MIU formal system that are n characters long.

%I A369410 #19 Jan 25 2024 15:02:43
%S A369410 1,4,4,2,13,13,8,13,8,8,11,11,6,11,6,6,11,6,6,6,3,12,12,18,12,18,18,
%T A369410 12,18,18,18,12,12,18,18,18,12,18,12,12,12,7,10,10,16,10,16,16,10,16,
%U A369410 16,16,10,10,16,16,16,10,16,10,10,10,5,10,16,16,16,10,16,10,10,10,5,16,10,10,10,5,10,10,5,10,5,5
%N A369410 Irregular triangle read by rows: row n lists the length of a "normal" proof (see comments) for each of the distinct derivable strings (theorems) in the MIU formal system that are n characters long.
%C A369410 See A368946 for the description of the MIU formal system, A369173 for the triangle of the corresponding strings (theorems) and A369409 for the definition of "normal" proof.
%D A369410 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
%H A369410 Paolo Xausa, <a href="/A369410/b369410.txt">Table of n, a(n) for n = 2..10922</a> (rows 2..14 of the triangle, flattened).
%H A369410 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 A369410 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369410 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%F A369410 T(n,k) >= A369408(n,k).
%F A369410 If A369173(n,k) contains no zeros and 3+2^m ones (for m >= 0), then T(n,k) = 4*m + 3.
%e A369410 Triangle begins:
%e A369410   [2]  1;
%e A369410   [3]  4  4  2;
%e A369410   [4] 13 13  8 13  8  8;
%e A369410   [5] 11 11  6 11  6  6 11  6  6  6  3;
%e A369410   ...
%e A369410 For the theorem MIU (310), which is given by A369173(3,2), the "normal" proof is MI (31) -> MII (311) -> MIIII (31111) -> MIU (310), which consists of 4 lines: T(3,2) is therefore 4.
%t A369410 MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
%t A369410 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 A369410 Map[MIUProofLineCount, Array[MIUDigitsW3, 7, 2], {2}]
%Y A369410 Row lengths of A369409.
%Y A369410 Cf. A368946, A369173, A369408, A369411, A369412.
%Y A369410 Cf. A024495 (row lengths).
%K A369410 nonn,tabf
%O A369410 2,2
%A A369410 _Paolo Xausa_, Jan 23 2024