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.

2, 13, 13, 5, 94, 94, 47, 94, 47, 47, 75, 75, 31, 75, 31, 31, 75, 31, 31, 31, 10, 120, 120, 165, 120, 165, 165, 120, 165, 165, 165, 90, 120, 165, 165, 165, 90, 165, 90, 90, 90, 43, 91, 91, 139, 91, 139, 139, 91, 139, 139, 139, 70, 91, 139, 139, 139, 70, 139, 70

Offset

2,1

Comments

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.

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).

References

Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.

Links

Paolo Xausa, Table of n, a(n) for n = 2..10922 (rows 2..14 of the triangle, flattened).

Armando B. Matos and Luis Filipe Antunes, Short Proofs for MIU theorems, Technical Report Series DCC-98-01, University of Porto, 1998.

Wikipedia, MU Puzzle.

Index entries for sequences from "Goedel, Escher, Bach".

Formula

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.

Example

Triangle begins:
  [2]  2;
  [3] 13 13  5;
  [4] 94 94 47 94 47 47;
  [5] 75 75 31 75 31 31 75 31 31 31 10;
  ...
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 4.

Mathematica

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

Crossrefs

Cf. A368946, A369173, A369408, A369409, A369410, A369413.

Cf. A369587 (analog for shortest proofs).

Cf. A024495 (row lengths).

Sequence in context: A037055 A065584 A153651 * A229908 A335972 A175270

Adjacent sequences: A369408 A369409 A369410 * A369412 A369413 A369414

Keyword

nonn,tabf

Author

Paolo Xausa, Jan 23 2024

Status

approved