|
%I #21 Jul 02 2024 03:08:30
%S 2,13,13,5,94,94,47,94,47,47,75,75,31,75,31,31,75,31,31,31,10,120,120,
%T 165,120,165,165,120,165,165,165,90,120,165,165,165,90,165,90,90,90,
%U 43,91,91,139,91,139,139,91,139,139,139,70,91,139,139,139,70,139,70
%N 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 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 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 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="/A369411/b369411.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 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 Triangle begins:
%e [2] 2;
%e [3] 13 13 5;
%e [4] 94 94 47 94 47 47;
%e [5] 75 75 31 75 31 31 75 31 31 31 10;
%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 a total of 13 symbols (counting only M, I and U characters): T(3,2) is therefore 13.
%t MIUDigitsW3[n_] := Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&];
%t 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 Map[MIUProofSymbolCount, Array[MIUDigitsW3, 7, 2], {2}]
%Y Cf. A368946, A369173, A369408, A369409, A369410, A369413.
%Y Cf. A369587 (analog for shortest proofs).
%Y Cf. A024495 (row lengths).
%K nonn,tabf,changed
%O 2,1
%A _Paolo Xausa_, Jan 23 2024
|
