A369413 -id:A369413 - 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.

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

Paolo Xausa, Jan 23 2024

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

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

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

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

Cf. A368946, A369173, A369408, A369409, A369410, A369413.
Cf. A369587 (analog for shortest proofs).
Cf. A024495 (row lengths).

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}]

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.

A369412 Maximum length of a "normal" proof (see comments) for strings (theorems) in the MIU formal system that are n characters long.

Original entry on oeis.org

1, 4, 13, 11, 18, 16, 25, 23, 24, 22, 26, 24, 34, 32, 33, 31, 35, 33, 34, 32, 39, 37, 49

Offset: 2

Paolo Xausa, Jan 23 2024

See A368946 for the description of the MIU formal system, A369410 for the triangle of the corresponding proof lengths and A369409 for the definition of "normal" proof.

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

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

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

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

a(n) = max_{k=1..A024495(n)} A369410(n,k).

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.

Views

Author

Keywords

Comments

Examples

References

Links

Crossrefs

Programs

Mathematica

Formula