A database of computational universality proofs, formalized and verified in Lean, validated and presented using Wolfram notebooks, all built and maintained by LLMs with only high-level expert guidance. This is to demonstrate that LLMs can autonomously push the boundary of mathematical research if they are given the right ingredients:
- ✅ Verification — Lean link to formalize and verify proofs
- ⚙️ Computational engine — Wolfram link to prototype and test on finite examples
- 📚 Knowledge base — a growing structured knowledge of the previous work (universality graph, wiki)
- 🧠 Expert guidance — high-level guidance by members of the Wolfram Institute
- 🤖 Agentic team member — autonomous agent homed at a Wolfram Institute server autonomously maintaining the repo and extending the research (TBD)
The generated data is organized as a universality graph: vertices are computational systems (Turing machines, cellular automata, tag systems, generalized shifts, ...) and directed edges are simulation encodings (weighted by overhead). We introduce this structure to empirically study the simulability landscape across simple machines in the spirit of Wolfram's metamathematics project and principle of computational equivalence.
| Notebook | Source | Wolfram Cloud |
|---|---|---|
| ECA Klein-4 Symmetries | Markdown | Notebook |
| TM ↔ Generalized Shift (Moore 1991) | Markdown | Notebook |
| Cocke–Minsky Chain (TM → Tag → CTS → (2,3) TM) | Markdown | Notebook |
| The Universality Graph | Markdown | Notebook |
| Cross-Validation (Lean vs. Wolfram) | Markdown | Notebook |
Edge wrappers live in Lean/Edges.lean; each carries its hypotheses explicitly in its type. Templates (Simulation, SimulationEncoding, HaltingSimulation) are explained in Wiki/Concepts/SimulationEncoding.md.
| Edge | Overhead (σ, τ) | Template | Reference | Sorry |
|---|---|---|---|---|
| ECA 110 ↔ 124, 137, 193 | 1, 1 | Simulation |
NKS p.55 | 0 |
| TM → Generalized Shift | 1, 1 | SimulationEncoding |
Moore 1991, Thm. 7 | 0 |
| Generalized Shift → TM | 1, ≤2(w−1)+m | SimulationEncoding |
Moore 1991, Thm. 8 | 0 |
| 2-Tag → Cyclic Tag | k, 2k | Simulation |
Cook 2004 | 0 (singleton-halting taken as hypothesis hHalt) |
| TM → 2-Tag | — | Simulation |
Cocke 1964 | axiomatized as hypothesis CockeMinskyStepSimulation |
| Cyclic Tag → (2,3) TM | — | HaltingSimulation |
Smith 2007 | axiomatized as hypothesis SmithSimulation |
The Cocke–Cook–Smith chain (last three rows) composes into edge_CockeMinskyChain, giving IsUniversal wolfram23 — universality of Wolfram's (2,3) TM, conditional on the two hypothesis arrows and on hHalt. See Wiki/Proofs/CockeMinskyChain.md.
- Read the theorem type in Lean/Edges.lean — every hypothesis is explicit.
- Read the machine definitions in Lean/Machines.
- Run the script below: rebuilds, audits axiom dependencies, replays through Lean's kernel.
- Cross-check on concrete examples in Wiki/Notebooks/CrossValidation.md.
Scripts/verify_integrity.shTrust model: Wiki/Concepts/ProofIntegrity.md
git clone --recurse-submodules <url>
cd Lean && lake build
Scripts/generate_notebooks.wls # Wiki/Notebooks/*.md → Notebooks/*.nb
leanblueprint web # interactive BlueprintWorkflow: CLAUDE.md · Next steps: Wiki/Plans/ActionItems.md
MIT