A368946 -id:A368946 - cp's OEIS frontend

A368947 Row lengths of A368946: in the MIU formal system, number of (possibly not distinct) strings n steps distant from the MI string.

Original entry on oeis.org

1, 2, 3, 6, 16, 60, 356, 3227, 44310, 928650, 28577371, 1296940642

Offset: 0

Paolo Xausa, Jan 10 2024

See A368946 for the description of the MIU formal system.

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

Wikipedia, MU Puzzle.
Index entries for sequences from "Goedel, Escher, Bach"

Cf. A331536, A368946, A368954.

MIUStepW3[s_] := Flatten[Map[{If[StringEndsQ[#, "1"], # <> "0", Nothing], # <> #, StringReplaceList[#, {"111" -> "0","00" -> ""}]}&, s]];
With[{rowmax = 9}, Map[Length, NestList[MIUStepW3, {"1"}, rowmax]]]

from itertools import islice
def occurrence_swaps(w, s, t):
    out, oi = [], w.find(s)
    while oi != -1:
        out.append(w[:oi] + t + w[oi+len(s):])
        oi = w.find(s, oi+1)
    return out
def moves(w): # moves for word w in MIU system, encoded as 310
    nxt = []
    if w[-1] == '1': nxt.append(w + '0')        # Rule 1
    if w[0] == '3': nxt.append(w + w[1:])       # Rule 2
    nxt.extend(occurrence_swaps(w, '111', '0')) # Rule 3
    nxt.extend(occurrence_swaps(w, '00', ''))   # Rule 4
    return nxt
def agen(): # generator of terms
    frontier = ['31']
    while len(frontier) > 0:
        yield len(frontier)
        reach1 = [m for p in frontier for m in moves(p)]
        frontier, reach1 = reach1, []
print(list(islice(agen(), 10))) # Michael S. Branicky, Jan 14 2024

a(n) >= A368954(n).

a(10)-a(11) from Michael S. Branicky, Jan 14 2024

A369173 Irregular triangle read by rows: row n lists all of the distinct derivable strings in the MIU formal system that are n characters long.

Original entry on oeis.org

31, 301, 310, 311, 3001, 3010, 3011, 3100, 3101, 3110, 30001, 30010, 30011, 30100, 30101, 30110, 31000, 31001, 31010, 31100, 31111, 300001, 300010, 300011, 300100, 300101, 300110, 301000, 301001, 301010, 301100, 301111, 310000, 310001, 310010, 310100, 310111, 311000, 311011, 311101, 311110, 311111

Offset: 2

Paolo Xausa, Jan 15 2024

See A368946 for the description of the MIU formal system.
A string S can be derived in the MIU formal system if and only if S contains just one M (as its first character) and an arbitrary number of I and U characters, where the number of I characters is not divisible by 3 (see Wikipedia link).
Strings are encoded using the map M -> 3, I -> 1 and U -> 0, and then sorted.
Row n has length A024495(n).

			Triangle begins:
  [2] 31;
  [3] 301 310 311;
  [4] 3001 3010 3011 3100 3101 3110;
  [5] 30001 30010 30011 30100 30101 30110 31000 31001 31010 31100 31111;
  ...

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).
Wikipedia, MU Puzzle.
Index entries for sequences from "Goedel, Escher, Bach".

Cf. A368946, A024495 (row lengths), A369174 (number of zeros), A369179 (number of ones), A369409.

Cf. A369586 (shortest proofs), A369408 (length of shortest proofs), A369587 (number of symbols of shortest proofs).

A369173row[n_] := Map[FromDigits[Join[{3}, #]]&, Select[Tuples[{0, 1}, n - 1], !Divisible[Count[#, 1], 3]&]]; Array[A369173row, 5, 2]

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

Paolo Xausa, Jan 23 2024

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.

			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.

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 = 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.
Index entries for sequences from "Goedel, Escher, Bach".

Cf. A368946, A369173, A369408, A369410 (row lengths), A369411, A369414.

Cf. A369586 (analog for shortest proofs).

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

A369408 Irregular triangle read by rows: T(n,k) is the length of the shortest proof for the MIU formal system string (theorem) given by A369173(n,k).

Original entry on oeis.org

1, 4, 2, 2, 11, 5, 8, 5, 8, 3, 9, 9, 6, 9, 5, 6, 9, 6, 3, 6, 3

Offset: 2

Paolo Xausa, Jan 22 2024

See A368946 for the description of the MIU formal system and A369173 for the triangle of the corresponding derivable strings.
The length of the shortest proof for a string (theorem) S is the number of lines of the shortest possible derivation of S.
A369173(n,k) first appears in row T(n,k) - 1 in triangle A368946.

			Triangle begins:
  [2]  1;
  [3]  4  2  2;
  [4] 11  5  8  5  8  3;
  [5]  9  9  6  9  5  6  9  6  3  6  3;
  ...
For the theorem MUI (301), which is given by A369173(3,1), the shortest derivation from the axiom MI is MI (31) -> MII (311) -> MIIII (31111) -> MIU (301) (4 lines), so T(3,1) = 4.

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

Wikipedia, MU Puzzle.
Index entries for sequences from "Goedel, Escher, Bach".

Cf. A024495 (row lengths), A331536, A368946, A369173, A369410.

Cf. A369586 (proofs), A369587 (number of symbols).

MIUStringsW3[n_] := Map[FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
MIUStepDW3[s_] := DeleteDuplicates[Flatten[Map[{If[StringEndsQ[#, "1"], # <> "0", Nothing], # <> #, StringReplaceList[#, {"111" -> "0", "00" -> ""}]} &, s]]];
Module[{rowmax = 5, treedepth = 10, tree}, tree = NestList[MIUStepDW3, {"1"}, treedepth]; Map[Quiet[Check[Position[tree, #, {2}][[1,1]], "Not found"]]&, Array[MIUStringsW3, rowmax - 1, 2], {2}]]

T(n,k) <= A369410(n,k).

A331536 Number of theorems in the MIU formal system which can be proved in n steps or fewer starting with the axiom 'mi'.

Original entry on oeis.org

1, 3, 6, 11, 25, 69, 282, 1730, 15885, 210105, 3986987, 106053474

Offset: 1

Brian Tenneson, Jan 19 2020

The MIU system was invented by Douglas Hofstadter and is found in his book Gödel, Escher, Bach.
In the MIU system words begin with the letter 'm' with the remaining letters being either 'u' or 'i'. Essentially, words can be represented by binary strings. It is given that 'mi' is a word. Thereafter, at each step words may be transformed by one of the following rules.
   1) Append a 'u' to a word ending in 'i'.
   2) Append a word to itself, excluding the initial 'm'.
   3) Replace an occurrence of 'iii' by 'u'.
   4) Remove an occurrence of 'uu'.

			The a(2) = 3 words that can be reached in at most one step are mi, miu, mii.
The a(3) = 6 words that can be reached in at most two steps are mi, miu, mii, miiii, miiu, miuiu.

Sean A. Irvine, Java program (github)
A. Matos, On the number of lines of theorems in the formal system MIU, Universidade do Porto, 2000, 1-10.
Wikipedia, Gödel, Escher, Bach
Wikipedia, MU Puzzle
Index entries for sequences from "Goedel, Escher, Bach"

Cf. A368946, A368953, A369148, A369173 (all MIU strings).

MIURules = {StartOfString ~~ x : _ ~~ "I" ~~ EndOfString :> x <> "IU", StartOfString ~~ "M" ~~ x : _ ~~ EndOfString :> "M" <> x <> x, "III" :> "U", "UU" :> ""}; (*The rules of the MIU formal system*)
MIUNext[s_String, rule_Integer] :=StringReplaceList[s, MIURules[[rule]]]
g[x_]:=DeleteDuplicates[Flatten[Join[{x},Table[Table[MIUNext[x[[j]],n], {n, 1, 4}],{j, 1,Length[x]}]]]]
a[n_Integer]:=Nest[g, "MI", n] // Length (*a[n] gives the number of theorems that can be proved in  n steps or fewer.  A331536[n]=a[n]. Remove //Length if you wish to see the theorems being counted.*)
(* Brian Tenneson, Sep 21 2023 *)

def occurrence_swaps(w, s, t):
  out, oi = [], w.find(s)
  while oi != -1:
    out.append(w[:oi] + t + w[oi+len(s):])
    oi = w.find(s, oi+1)
  return out
def moves(w): # moves for word w in miu system
  nxt = [w + w] # Rule 2 ('m' not stored; else use nxt = [w + w[1:]])
  if w[-1] == 'i': nxt.append(w + 'u')       # Rule 1
  nxt.extend(occurrence_swaps(w, 'iii', 'u')) # Rule 3
  nxt.extend(occurrence_swaps(w, 'uu', ''))   # Rule 4
  return nxt
def alst(maxd=float('inf'), v=False):
  alst, d = [], 0
  reached, frontier = {'i'}, {'i'} # don't store 'm's (else use 'mi' twice)
  alst.append(len(reached))
  if v: print(len(reached), end=", ")
  while len(frontier) > 0 and d < maxd:
    reach1 = set(m for p in frontier for m in moves(p) if m not in reached)
    if v: print(len(reached)+len(reach1), end=", ")
    alst.append(len(reached)+len(reach1))
    reached |= reach1
    frontier = reach1
    d += 1
  return alst
alst(maxd=10, v=True) # Michael S. Branicky, Dec 29 2020

a(11) from Rémy Sigrist, Feb 26 2020
a(12) from Sean A. Irvine, Mar 20 2020
Name edited by Brian Tenneson, Aug 19 2023

A369586 Irregular triangle read by rows: row n lists the lines of the shortest proof for the MIU formal system string (theorem) given by A369173(n+1).

Original entry on oeis.org

31, 31, 311, 31111, 301, 31, 310, 31, 311, 31, 311, 31111, 311111111, 3011111, 30011, 300110011, 3001100110, 30011110, 300100, 3001, 31, 311, 31111, 301, 3010, 31, 311, 31111, 311111111, 3011111, 30111110, 301100, 3011, 31, 311, 31111, 311110, 3100, 31, 311, 31111, 311111111, 3101111, 31011110, 310100, 3101, 31, 311, 3110

Offset: 1

Paolo Xausa, Jan 26 2024

See A368946 for the description of the MIU formal system.
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.

			Triangle begins:
  [1] 31;
  [2] 31 311 31111 301;
  [3] 31 310;
  [4] 31 311;
  [5] 31 311 31111 ... 30011 300110011 3001100110 30011110 300100 3001;
  ...
For the theorem MUI (301), which is given by A369173(3,1) or (after flattening) A369173(3), the shortest proof is 31 -> 311 -> 31111 -> 301, which is row 2 of the present sequence (same as the "normal" proof, cf. A369409).
For the theorem MIUU (3100), which is given by A369173(4,4) or (after flattening) A369173(9), the shortest proof is 31 -> 311 -> 31111 -> 311110 -> 3100, which is row 8 of the present sequence (shorter than the "normal" proof).

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 = 1..120 (rows 1..21 of the triangle, flattened).
Wikipedia, MU Puzzle.
Index entries for sequences from "Goedel, Escher, Bach".

Cf. A368946, A369173, A369409 (analog for "normal" proofs).

Cf. A369408 (row lengths), A369587 (number of symbols).

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, If[# == mi, {#}, First[Sort[FindPath[g, mi, #, {GraphDistance[g, mi, #]}, All]]]]], {"Not found"}]] &, Flatten[Array[MIUStrings, uptolen - 1, 2]]]] (* Considers theorems up to 5 characters long, looking up to 10 steps away from the MI axiom -- please note it takes a while *)

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

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.

			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.

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

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

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

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.

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.

Original entry on oeis.org

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.

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

Paolo Xausa, Jan 26 2024

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.

			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.

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

Wikipedia, MU Puzzle.
Index entries for sequences from "Goedel, Escher, Bach".

Cf. A368946, A369173, A369411 (analog for "normal" proofs).

Cf. A024495 (row lengths), A369408 (number of lines), A369586 (proofs).

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

A368953 Irregular triangle read by rows: row n lists (in lexicographical order and with duplicates removed) the strings of the MIU formal system at the n-th level of the tree generated by recursively applying the system rules, starting from the MI string.

Original entry on oeis.org

31, 310, 311, 31010, 3110, 31111, 301, 310, 310101010, 3110110, 311110, 311111111, 3010, 30101, 3011111, 3100, 31010, 31010101010101010, 3101111, 3110110110110, 3110111, 3111011, 3111101, 31111011110, 3111110, 3111111110, 31111111111111111

Offset: 0

Paolo Xausa, Jan 10 2024

This is a variant of A368946 (see there for the description of the MIU system) where, within a row, duplicates are removed and encoded strings are ordered lexicographically.

			After recursively applying the rules three times, we get the following tree (cf. Hofstadter (1979), page 40, Figure 11).
.
                           MI
  0 ---------------------- 31
                         /    \
                        1      2 <--- Rule applied
                       /        \
                     MIU        MII
  1 ---------------- 310        311
                    /          /   \
                   2          1     2
                  /          /       \
              MIUIU       MIIU      MIIII
  2 --------- 31010       3110      31111
               /          /       / |   | \
              2          2       1  2   3  3
             /          /       /   |   |   \
        MIUIUIUIU   MIIUIIU  MIIIIU |  MUI  MIU
  3 --- 310101010   3110110  311110 |  301  310
                                MIIIIIIII
                                311111111
.
After ordering the encoded strings lexicographically within a tree level (and removing duplicates, if present), the triangle begins:
  [0] 31;
  [1] 310 311;
  [2] 31010 3110 31111;
  [3] 301 310 310101010 3110110 311110 311111111;
  ...
Please note that some strings may be present in different rows: within the first four rows, the string MIU (310) is present in rows 1 and 3.

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 = 0..16809 (rows 0..8 of the triangle, flattened).
Wikipedia, MU Puzzle
Index entries for sequences from "Goedel, Escher, Bach"

Cf. A331536, A368946, A368954 (row lengths), A369173 (all MIU strings).

MIUStepL[s_] := Union[Flatten[Map[{If[StringEndsQ[#, "1"], # <> "0", Nothing], # <> StringDrop[#, 1], StringReplaceList[#, {"111" -> "0", "00" -> ""}]}&, s]]];
With[{rowmax = 4}, Map[FromDigits, NestList[MIUStepL, {"31"}, rowmax], {2}]]

cp's OEIS Frontend

A368947 Row lengths of A368946: in the MIU formal system, number of (possibly not distinct) strings n steps distant from the MI string.

Views

Author

Keywords

Comments

References

Links

Crossrefs

Programs

Mathematica

Python

Formula

Extensions

A369173 Irregular triangle read by rows: row n lists all of the distinct derivable strings in the MIU formal system that are n characters long.

Views

Author

Keywords

Comments

Examples

References

Links

Crossrefs

Programs

Mathematica

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

Views

Author

Keywords

Comments

Examples

References

Links

Crossrefs

Programs

Mathematica

A369408 Irregular triangle read by rows: T(n,k) is the length of the shortest proof for the MIU formal system string (theorem) given by A369173(n,k).

Views

Author

Keywords

Comments

Examples

References

Links

Crossrefs

Programs

Mathematica

Formula

A331536 Number of theorems in the MIU formal system which can be proved in n steps or fewer starting with the axiom 'mi'.

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

Programs

Mathematica

Python

Extensions

A369586 Irregular triangle read by rows: row n lists the lines of the shortest proof for the MIU formal system string (theorem) given by A369173(n+1).

Views

Author

Keywords

Comments

Examples

References

Links

Crossrefs

Programs

Mathematica

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.

Views

Author

Keywords

Comments

Examples

References

Links

Crossrefs