login
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.
5

%I #19 Jan 25 2024 15:02:43

%S 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 12,18,18,18,12,12,18,18,18,12,18,12,12,12,7,10,10,16,10,16,16,10,16,

%U 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 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 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 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.

%H 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 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 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.

%H <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.

%F T(n,k) >= A369408(n,k).

%F If A369173(n,k) contains no zeros and 3+2^m ones (for m >= 0), then T(n,k) = 4*m + 3.

%e Triangle begins:

%e [2] 1;

%e [3] 4 4 2;

%e [4] 13 13 8 13 8 8;

%e [5] 11 11 6 11 6 6 11 6 6 6 3;

%e ...

%e 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 MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];

%t 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 Map[MIUProofLineCount, Array[MIUDigitsW3, 7, 2], {2}]

%Y Row lengths of A369409.

%Y Cf. A368946, A369173, A369408, A369411, A369412.

%Y Cf. A024495 (row lengths).

%K nonn,tabf

%O 2,2

%A _Paolo Xausa_, Jan 23 2024