OFFSET
1,1
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.
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 = 1..10823 (rows 1..682 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.
EXAMPLE
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.
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}]
CROSSREFS
KEYWORD
nonn,tabf
AUTHOR
Paolo Xausa, Jan 23 2024
STATUS
approved