Notation.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

19 declarations, 0 contain sorry, 0 declared as axioms

Turing Machine Parser

This module provides a parser for defining a Turing machine from a simple string description. The main entry point is the turing_machine% elaborator, which takes a string representing the machine's transitions and constructs a term of type Machine (Fin m) StateType where StateType is an inductive type generated on the fly.

Encoding format

The machine's transitions are encoded as a single string, with each state's transitions separated by an underscore (_). For each state, a 3m-character substring defines the behavior:

The first 3 characters "ABC" describe the action when the head reads 0:
- A: The symbol to write (0, 1, ..., m-1).
- B: The direction to move the head (L or R).
- C: The new state (A through Z).
The next 3 characters "DEF" describe the action when the head reads 1 using the same format.
The next 3 characters "GHI" describe the action when the head reads 2 using the same format.
So on...

The character Z is reserved for the halting state. The string "---" can be used to represent a transition to the halting state without writing or moving.

Example of a tape: 1RA0LB_0LA---

There are more examples at the end of this file.

Imports (3)

Imported by 1 file

FormalConjecturesForMathlib.lean

def Alphabet line 58 source

def Char.toDirSyntax Char.toDirSyntax c outputs the syntax corresponding to the character c if c is R or L and throws an error in other cases line 64 source

Source documentation

Char.toDirSyntax c outputs the syntax corresponding to the character c if c is R or L and throws an error in other cases. This is used when parsing the "direction" component of turing machine string representations.

private def Char.toDirSyntax : Char → TermElabM Term
  | 'R' => `(Dir.right)
  | 'L' => `(Dir.left)
  | char => throwError "Invalid direction {char}."

/-- `Char.toBinarySyntax c` outputs the syntax corresponding to the character `c` if `c` is in
`0, ..., 9` and throws an error in other cases. This is used when parsing the "symbol"
component of turing machine string representations. -/

Mentions: c

def Char.toNumeralSyntax Char.toBinarySyntax c outputs the syntax corresponding to the character c if c is in 0, ..., 9 and throws an error in other cases line 72 source
Source documentation
Char.toBinarySyntax c outputs the syntax corresponding to the character c if c is in 0, ..., 9 and throws an error in other cases. This is used when parsing the "symbol" component of turing machine string representations.
```
private def Char.toNumeralSyntax (c : Char) : TermElabM Term := do
…
```
Mentions: c
def Char.toStateSyntax Char.toStateSyntax c stateName outputs the syntax of the constructor corresponding to c if c is a capital letter (i.e. something between A and Z.) line 83 source
Source documentation
Char.toStateSyntax c stateName outputs the syntax of the constructor corresponding to c if c is a capital letter (i.e. something between A and Z.). For example, A would output the syntax stateName.A where stateName is the name of the type used to index sets. This is used when parsing the "state" component of turing machine string representations.
```
private def Char.toStateSyntax (c : Char) (stateName : Name) (numStates : Nat) : TermElabM Term := do
…
```
Mentions: c
def Nat.toStateSyntax Nat.toStateSyntax n stateName outputs the syntax of the n-th constructor of the type used to index states line 95 source
Source documentation
Nat.toStateSyntax n stateName outputs the syntax of the n-th constructor of the type used to index states.
```
private def Nat.toStateSyntax (n : Nat) (stateName : Name) : TermElabM Term := do
…
```
def String.toStmtSyntax String.toStmtSyntax s stateName parses a component of a Turing machine string representation and outputs the syntax of the corresponding (state, statement) : State × Stmt pair line 102 source
Source documentation
String.toStmtSyntax s stateName parses a component of a Turing machine string representation and outputs the syntax of the corresponding (state, statement) : State × Stmt pair.
```
private def String.toStmtSyntax (s : String) (stateName : Name) (numStates : Nat) : TermElabM Term := do
…
```
def String.nextn line 116 source
def mkMachineMatchAltExpr Documented declaration: mkMachineMatchAltExpr line 125 source
Source documentation
Take as input a list of strings and return an array of matchAltExpr syntaxes mapping (state, symbol) pairs to actions of a Turing Machine, given by a term of type Option (State n).
```
def mkMachineMatchAltExpr (L : List String) (stateName : Name) (numSymbols numStates: Nat) :
    TermElabM (Array (TSyntax ``matchAltExpr)) := do
…
```
def Nat.toStateName The name of the state type with n constructors A, B, ... line 147 source
Source documentation
The name of the state type with n constructors A, B, ....
```
private def Nat.toStateName (n : Nat) : Name := .mkSimple s!"State{n}"
…
```
def mkStateType Documented declaration: mkStateType line 160 source
Source documentation
mkStateType n adds to the environment an inductive type with n states names State{n} with constructors the symbols A, B, ..., together with the instance Inhabited (State{n}).
Both declarations have to be public. liftCommandElabM runs them in a fresh scope that does not carry the surrounding module's visibility, so without it they are declared private and end up named _private.<module>.0.State{n}. The lookup below then fails with Unknown constant State{n}, and the type would in any case be private while appearing in the type of the term this elaborator returns.

L4DEL explanation
mkStateType n adds to the environment an inductive type with n states names State{n} with constructors the symbols A, B, ..., together with the instance Inhabited (State{n}). Both declarations have to be public. liftCommandElabM runs them in a fresh scope that does not carry the surrounding module's visibility, so without it they are declared private and end up named _private..0.State{n}. The lookup below then fails with Unknown constant State{n}, and the type would in any case be private while appearing in the type of the term this elaborator returns.
Sources and attribution: Pinned Lean source (1646ca16afd6)
```
def mkStateType (n : ℕ) (stateName : Name) : TermElabM Unit := do
…
```
def parseTuring parseTuring tmStringDescription outputs the Expr corresponding to the Turing Machine described by the string tmStringDescription line 189 source
Source documentation
parseTuring tmStringDescription outputs the Expr corresponding to the Turing Machine described by the string tmStringDescription.
To do so, it
1. Runs mkStateType to add the state type to the environment
2. Defines the corresponding Turing Machine as a function using the match syntax.
Warning: if a state type (i.e. something with the name State1, State2, ...) already exists in the environment then this will be reused without checking that this is the right inductive type - such checks are left to the user.
```
def parseTuring (descr : String) : TermElabM Expr := do
…
```
example (example at line 231) line 231 source
example (example at line 234) line 234 source
example (example at line 242) line 242 source
example (example at line 250) line 250 source
example (example at line 288) line 288 source
Source comment
A machine with no transitions halts after zero steps.
```
example : IsHalting (turing_machine% "------") :=
…
```
example (example at line 292) line 292 source
Source comment
A machine that moves to a state without transitions halts after one step.
```
example : IsHalting (turing_machine% "0RB0RB_------") :=
…
```
example (example at line 295) line 295 source
example (example at line 302) line 302 source
Source comment
A machine whose transitions never enter the halting state does not halt.
```
example : ¬ IsHalting (turing_machine% "0RB0LB_0RA0LB") := by
…
```