cp's OEIS Frontend

A369411 Irregular triangle read by rows: row n lists the number of symbols 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 A369411 #21 Jul 02 2024 03:08:30
%S A369411 2,13,13,5,94,94,47,94,47,47,75,75,31,75,31,31,75,31,31,31,10,120,120,
%T A369411 165,120,165,165,120,165,165,165,90,120,165,165,165,90,165,90,90,90,
%U A369411 43,91,91,139,91,139,139,91,139,139,139,70,91,139,139,139,70,139,70
%N A369411 Irregular triangle read by rows: row n lists the number of symbols 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 A369411 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.
%C A369411 The number of symbols of a proof is the sum of the number of characters contained in all of the strings (lines) of the proof; cf. Matos and Antunes (1998).
%D A369411 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
%H A369411 Paolo Xausa, <a href="/A369411/b369411.txt">Table of n, a(n) for n = 2..10922</a> (rows 2..14 of the triangle, flattened).
%H A369411 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 A369411 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369411 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%F A369411 If A369173(n,k) contains no zeros and 3+2^m ones (for m >= 0), then T(n,k) = 2^(m+3) + 25*m + 2.
%e A369411 Triangle begins:
%e A369411   [2]  2;
%e A369411   [3] 13 13  5;
%e A369411   [4] 94 94 47 94 47 47;
%e A369411   [5] 75 75 31 75 31 31 75 31 31 31 10;
%e A369411   ...
%e A369411 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 a total of 13 symbols (counting only M, I and U characters): T(3,2) is therefore 13.
%t A369411 MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
%t A369411 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 A369411 Map[MIUProofSymbolCount, Array[MIUDigitsW3, 7, 2], {2}]
%Y A369411 Cf. A368946, A369173, A369408, A369409, A369410, A369413.
%Y A369411 Cf. A369587 (analog for shortest proofs).
%Y A369411 Cf. A024495 (row lengths).
%K A369411 nonn,tabf
%O A369411 2,1
%A A369411 _Paolo Xausa_, Jan 23 2024