cp's OEIS Frontend

This is a front-end for the Online Encyclopedia of Integer Sequences, made by Christian Perfect. The idea is to provide OEIS entries in non-ancient HTML, and then to think about how they're presented visually. The source code is on GitHub.

Showing 1-4 of 4 results.

A369409 Irregular triangle read by rows: row n lists the lines of a "normal" proof (see comments) for the MIU formal system string (theorem) given by A369173(n+1).

Original entry on oeis.org

31, 31, 311, 31111, 301, 31, 311, 31111, 310, 31, 311, 31, 311, 31111, 311111111, 3111111110, 31111100, 311111, 31111111111, 311111111110, 3111111100, 31111111, 311101, 3001, 31, 311, 31111, 311111111, 3111111110, 31111100, 311111, 31111111111, 311111111110, 3111111100, 31111111
Offset: 1

Views

Author

Paolo Xausa, Jan 23 2024

Keywords

Comments

See A368946 for the description of the MIU formal system.
Matos and Antunes (1998) define a "normal" proof for a string (theorem) S the output of the following algorithm, which generates the lines (strings) of the proof.
Step 1. Replace in turn every occurrence of U in S by III.
Step 2. Until we get MI:
Step 2a. If the number of I characters is even, remove half of them.
Step 2b. Otherwise, apply in turn the following transformations: append UU, replace the first U by III, remove the remaining U, remove half of the I characters.
Step 3. Reverse the order of the lines.
This algorithm generates a short proof, but not necessarily the shortest one.
Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.

Examples

			Triangle begins:
  [1] 31;
  [2] 31 311 31111 301;
  [3] 31 311 31111 310;
  [4] 31 311;
  [5] 31 311 31111 ... 31111100 ... 31111111111 ... 3111111100 31111111 311101 3001;
  ...
For the theorem MUI (301), which is given by A369173(3,1) or (after flattening) A369173(3), steps 1 and 2 of the algorithm generate the lines 301 -> 31111 -> 311 -> 31 which, when reversed (step 3), give row 2 of the present sequence.
For the theorem MIUU (3100), which is given by A369173(4,4) or (after flattening) A369173(9), steps 1 and 2 of the algorithm generate the lines 3100 -> 311110 -> 31111111 -> 3111111100 -> 311111111110 -> 31111111111 -> 311111 -> 31111100 -> 3111111110 -> 311111111 -> 31111 -> 311 -> 31 which, when reversed (step 3), give row 8 of the present sequence.

References

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

Links

Crossrefs

Cf. A368946, A369173, A369408, A369410 (row lengths), A369411, A369414.
Cf. A369586 (analog for shortest proofs).

Programs

  • Mathematica
    MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&]];
MIUProofLines[t_] := Module[{s = t}, Reverse[Flatten[Reap[Sow[s]; While[StringCount[s, "0"] > 0, Sow[s = StringReplace[s, "0" -> "111", 1]]]; While[s != "31", If[EvenQ[StringCount[s, "1"]], Sow[s = StringDrop[s, -(StringLength[s]-1)/2]], Sow[{s <> "00", s <> "1110", s <> "111", s = StringDrop[s, -(StringLength[s]-4)/2]}]]]][[2,1]]]]];
Map[FromDigits, Map[MIUProofLines, Flatten[Array[MIUStrings, 3, 2]]], {2}]

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

Original entry on oeis.org

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, 12, 18, 18, 18, 12, 12, 18, 18, 18, 12, 18, 12, 12, 12, 7, 10, 10, 16, 10, 16, 16, 10, 16, 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
Offset: 2

Views

Author

Paolo Xausa, Jan 23 2024

Keywords

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.

Examples

			Triangle begins:
  [2]  1;
  [3]  4  4  2;
  [4] 13 13  8 13  8  8;
  [5] 11 11  6 11  6  6 11  6  6  6  3;
  ...
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.

References

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

Links

Crossrefs

Row lengths of A369409.
Cf. A368946, A369173, A369408, A369411, A369412.
Cf. A024495 (row lengths).

Programs

  • Mathematica
    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[MIUProofLineCount, Array[MIUDigitsW3, 7, 2], {2}]

Formula

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

A369587 Irregular triangle read by rows: row n lists the number of symbols of the shortest proof (see comments) for each of the distinct derivable strings (theorems) in the MIU formal system that are n characters long.

Original entry on oeis.org

2, 13, 5, 5, 68, 17, 44, 20, 44, 9, 52, 52, 31, 52, 18, 31, 52, 31, 10, 31, 10
Offset: 2

Views

Author

Paolo Xausa, Jan 26 2024

Keywords

Comments

See A368946 for the description of the MIU formal system and A369173 for the triangle of corresponding strings.
Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.
In case more than one shortest proof exists, the lexicographically earliest one (after encoding) is chosen.

Examples

			Triangle begins:
  [2]  2;
  [3] 13  5  5;
  [4] 68 17 44 20 44  9;
  [5] 52 52 31 52 18 31 52 31 10 31 10;
  ...
For the theorem MIUU (3100), which is given by A369173(4,4), the shortest proof is MI (31) -> MII (311) -> MIIII (31111) -> MIIIIU (311110) -> MIUU (3100), which consists of a total of 20 symbols (counting only M, I and U characters): T(4,4) is therefore 20.

References

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

Links

Crossrefs

Cf. A368946, A369173, A369411 (analog for "normal" proofs).
Cf. A024495 (row lengths), A369408 (number of lines), A369586 (proofs).

Programs

  • Mathematica
    MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48] &, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
MIUNext[s_] := Flatten[{If[StringEndsQ[s, "1"], s <> "0", Nothing], s <> StringDrop[s, 1], StringReplaceList[s, {"111" -> "0", "00" -> ""}]}];
Module[{uptolen = 5, searchdepth = 10, mi = "31", g}, g = NestGraph[MIUNext, mi, searchdepth]; Map[Quiet[Check[Map[FromDigits, StringLength[StringJoin[If[# == mi, #, First[Sort[FindPath[g, mi, #, {GraphDistance[g, mi, #]}, All]]]]]]], "Not found"]] &, Array[MIUStrings, uptolen - 1, 2], {2}]] (* Considers theorems up to 5 characters long, looking up to 10 steps away from the MI axiom -- please note it takes a while *)

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

Original entry on oeis.org

2, 13, 94, 75, 165, 139, 308, 269, 348, 299, 482, 423, 647, 581, 780, 701, 893, 807, 1064, 965, 1281, 1175, 1654
Offset: 2

Views

Author

Paolo Xausa, Jan 23 2024

Keywords

Comments

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

References

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

Links

Crossrefs

Cf. A024495, A368946, A369173, A369409, A369411, A369412.

Programs

  • 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[Max, Map[MIUProofSymbolCount, Array[MIUDigitsW3, 15, 2], {2}]]

Formula

a(n) = max_{k=1..A024495(n)} A369411(n,k).
Showing 1-4 of 4 results.

Started in 1964 by Neil J. A. Sloane | Maintained by The OEIS Foundation Inc.

Content is available under The OEIS End-User License Agreement.