{"path":"research/lean4-proof-assistant-deep-dive.md","content":"# Lean 4 Proof Assistant: Deep Architectural Research\n\n**Date**: 2026-03-28\n**Context**: Deliberus project — understanding the \"proposer + verifier\" architecture pattern, formal verification as community artifact, and implications for collaborative knowledge systems.\n\n---\n\n## 1. Architecture: Kernel, Elaboration, and the Trust Boundary\n\n### The Trusted Kernel\n\nLean follows the **LCF (Logic for Computable Functions) architecture**, originating from Edinburgh in the 1970s. The core idea: there is a **small trusted kernel** that defines what constitutes a valid proof. Everything else — tactics, automation, metaprograms, UI — is **untrusted code** that must ultimately produce artifacts the kernel accepts.\n\nLean's kernel checks **proof terms**: specific data structures (of type `Expr`) that encode an entire logical argument from axioms to conclusion. The kernel verifies that a proof term is a valid construction in Lean's type theory. It is deliberately small (~5,000 lines of C++ code) so that it can be audited and trusted.\n\n**What the kernel checks:**\n- Type correctness: every expression has a well-formed type\n- Definitional equality: computationally equivalent expressions are treated as equal\n- Universe consistency: no circular type hierarchies (no `Type : Type`)\n- Inductive type well-formedness: recursion is well-founded (strict positivity check)\n\n**What the kernel does NOT do:**\n- Proof search (that's tactics)\n- Parsing or syntax (that's the elaborator)\n- Automation (that's metaprogramming)\n- Pretty-printing (that's the formatter)\n\nThis is the **proposer-verifier pattern** at its most fundamental: the entire rest of the system (elaborator, tactics, metaprograms, user code) is the *proposer*. The kernel is the *verifier*. You can have arbitrarily buggy, creative, or AI-generated code in the proposer layer — if the kernel accepts the proof term, the proof is correct.\n\n### The Elaboration Layer\n\nBetween user-facing syntax and the kernel sits the **elaborator**: the component that turns human-readable `Syntax` objects into kernel-checkable `Expr` terms. This is where most of the complexity lives.\n\nThe elaboration process:\n1. **Parsing**: Lean's extensible parser turns source text into `Syntax` trees\n2. **Macro expansion**: Syntactic sugar is expanded (e.g., `do` notation, `where` clauses)\n3. **Term elaboration**: `Syntax` is translated into `Expr` (the kernel's internal representation), filling in implicit arguments, resolving overloaded notation, inserting coercions\n4. **Tactic elaboration**: If the user wrote `by ...`, the tactic block is executed to produce an `Expr`\n5. **Kernel check**: The final `Expr` is submitted to the kernel for verification\n\nThe elaborator uses **metavariables** (written `?m`) as placeholders — holes in expressions that get filled in during elaboration. This is how Lean handles implicit arguments, type inference, and the connection between tactics and proof terms.\n\n### The Monad Stack\n\nLean's metaprogramming API is organized as a hierarchy of monads:\n\n- **`CoreM`**: Access to the environment (all declarations/imports). The thinnest layer.\n- **`MetaM`**: Access to the metavariable context. Can create metavariables, assign them, check definitional equality, reduce expressions to weak head normal form (WHNF). This is where \"giving meaning to expressions\" happens.\n- **`TermElabM`**: Access to elaboration state. Extends `MetaM` with information needed during term elaboration (expected types, pending obligations).\n- **`TacticM`**: Access to the list of current goals. Extends `TermElabM`. All tactics are `TacticM Unit`.\n\nEach monad extends the ones below it, so a `TacticM` computation can use metavariable operations, and a `MetaM` computation can access the environment.\n\n### Core Logic\n\nLean's type theory has exactly three primitive constructions:\n1. **Universes**: `Prop = Sort 0`, `Type = Sort 1`, `Type 1 = Sort 2`, etc.\n2. **Dependent function types** (Pi types): `(x : A) -> B x` — when `B` doesn't depend on `x`, this is ordinary `A -> B`\n3. **Inductive types**: The mechanism for defining new types with constructors and recursion\n\nPlus three axioms for classical mathematics:\n- **Propositional extensionality**: `(a <-> b) -> a = b` for propositions\n- **Quotient types**: Which imply function extensionality\n- **Choice**: `Nonempty a -> a` (the axiom of choice, which gives classical logic via Diaconu's theorem: `forall P, P \\/ not P`)\n\nEverything else — `And`, `Or`, `Exists`, `True`, `False`, natural numbers, lists, structures — is defined using inductive types. Logic literally emerges from the type system.\n\n**Sources**: [Avigad's Hausdorff School lecture notes](https://gist.github.com/avigad/1316b67a27fab2865cf8ef3993fd5e27), [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/), [Metaprogramming in Lean 4](https://leanprover-community.github.io/lean4-metaprogramming-book/)\n\n---\n\n## 2. The Tactic System: How Humans Write Machine-Checked Proofs\n\n### Tactics as Goal Manipulation\n\nA **tactic** is a program that manipulates proof goals. Under the hood, goals are metavariables: each has a local context (hypotheses) and a target type (what needs to be proved). A tactic transforms the current set of goals into (hopefully simpler) sub-goals.\n\nExample: proving `f (f a) = a` given `h : forall a, f a = a`:\n\n```lean\nexample (h : forall a, f a = a) : f (f a) = a := by\n  apply Eq.trans   -- creates two subgoals: f(f a) = ?b and ?b = a\n  apply h          -- solves first subgoal, unifying ?b with f a\n  apply h          -- solves second subgoal\n```\n\nWhat happens internally:\n1. Lean creates metavariable `?m1` with target `f (f a) = a`\n2. `apply Eq.trans` creates `?m2` (target `f (f a) = ?b`), `?m3` (target `?b = a`), `?m4` (target type `alpha`), and assigns `?m1 := Eq.trans ?m2 ?m3`\n3. `apply h` on `?m2` unifies and assigns `?m2 := h (f a)`, which also determines `?b := f a`\n4. `apply h` on `?m3` assigns `?m3 := h a`\n5. All metavariables are assigned. The final proof term is `Eq.trans (h (f a)) (h a)`\n\n**The proof term is what the kernel checks.** Tactics are just a convenient way to construct it incrementally.\n\n### Tactic Proofs vs Term Proofs\n\nThe same theorem can be proved in \"term mode\" (directly constructing the proof term) or \"tactic mode\" (using `by`):\n\n```lean\n-- Term mode: you write the proof term directly\ntheorem and_comm : P /\\ Q -> Q /\\ P :=\n  fun h => And.intro h.right h.left\n\n-- Tactic mode: you manipulate goals\ntheorem and_comm' : P /\\ Q -> Q /\\ P := by\n  intro h\n  exact And.intro h.right h.left\n```\n\nBoth produce the same proof term. The kernel doesn't know or care which mode was used.\n\n### Tactics Are Just Lean Programs\n\nA critical Lean 4 design decision: **tactics are written in Lean itself**. The type `TacticM` is:\n\n```lean\nTacticM = ReaderT Context $ StateRefT State TermElabM\n```\n\nYou can write new tactics as ordinary Lean functions. You can inspect existing tactics' source code. There is no separate \"tactic metalanguage\" (contrast with Coq's Ltac, which is a different language from Gallina).\n\nTactics can be extended via macro expansion:\n```lean\n-- Declare an extensible tactic\nsyntax \"custom_tactic\" : tactic\n\n-- Add rfl as one behavior\nmacro_rules\n| `(tactic| custom_tactic) => `(tactic| rfl)\n\n-- Later, extend it further\nmacro_rules\n| `(tactic| custom_tactic) => `(tactic| apply And.intro <;> custom_tactic)\n```\n\nThis extensibility is what makes Lean's tactic system so powerful for building domain-specific automation.\n\n**Sources**: [Metaprogramming in Lean 4, Chapter 9: Tactics](https://leanprover-community.github.io/lean4-metaprogramming-book/main/09_tactics.html), [Metaprogramming in Lean 4, Chapter 4: MetaM](https://leanprover-community.github.io/lean4-metaprogramming-book/main/04_metam.html)\n\n---\n\n## 3. Curry-Howard Correspondence: Types as Propositions, Programs as Proofs\n\n### The Core Insight\n\nIn dependent type theory, there is no separate \"logic layer.\" The same language handles data, computation, and proof:\n\n| Concept | Programming View | Logic View |\n|---------|-----------------|------------|\n| Type | Data type | Proposition |\n| Term | Program/value | Proof |\n| `A -> B` | Function type | Implication |\n| `(x : A) -> B x` | Dependent function | Universal quantification |\n| `A x B` (product) | Pair type | Conjunction (and) |\n| `A + B` (sum) | Either type | Disjunction (or) |\n| Empty type | Uninhabited | False |\n| Unit type | Singleton | True |\n| Function application | Computation | Modus ponens |\n| Lambda abstraction | Function definition | Implication introduction |\n\nThis means:\n- A **definition** returns an element of a type: `def a : Nat := 2`\n- A **theorem** returns a proof of a proposition: `theorem foo : 2 + 2 = 4 := rfl`\n- These are syntactically almost identical. The main difference: theorems are marked **opaque** (their proof terms aren't unfolded during type-checking of other terms).\n\n### How Logic Emerges from Inductive Types\n\nAll logical connectives are defined as inductive types in Lean's core library:\n\n```lean\ninductive False : Prop           -- no constructors = no proof possible\n\ninductive True : Prop\n| intro : True                   -- trivially provable\n\ninductive And (a b : Prop) : Prop\n| intro : a -> b -> And a b      -- need proofs of both\n\ninductive Or (a b : Prop) : Prop\n| inl : a -> Or a b              -- proof of left suffices\n| inr : b -> Or a b              -- proof of right suffices\n\ninductive Exists {a : Type*} (q : a -> Prop) : Prop\n| intro : forall (a : a), q a -> Exists q   -- witness + proof\n```\n\nThis is not an encoding trick — it is the actual implementation. `And.intro` is literally a constructor that takes two proofs and produces a proof of the conjunction.\n\n### Definitional Equality\n\nTwo expressions are **definitionally equal** (defeq) if they compute to the same normal form. The kernel treats defeq expressions as interchangeable without explicit proof. This includes:\n- Beta reduction: `(fun x => f x) a` defeq `f a`\n- Delta reduction: unfolding definitions\n- Iota reduction: pattern matching on constructors\n- Eta expansion: `f` defeq `fun x => f x`\n\nDefinitional equality is checked by `isDefEq` in MetaM, which uses heuristics to avoid computing full normal forms (which can be very expensive).\n\n**Sources**: [Lean 4 Theorem Proving, Ch. 2: Dependent Type Theory](https://lean-lang.org/theorem_proving_in_lean4/Dependent-Type-Theory/), [Lean 4 Theorem Proving, Ch. 3: Propositions and Proofs](https://lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs/), [Avigad lecture notes](https://gist.github.com/avigad/1316b67a27fab2865cf8ef3993fd5e27)\n\n---\n\n## 4. Mathlib: The Largest Coherent Mathematical Library\n\n### Scale and Scope\n\nAs of late 2025, Mathlib contains:\n- **~1.9 million lines** of Lean 4 code\n- **~130,000+ premises** (theorems, lemmas, definitions)\n- Coverage spanning undergraduate and graduate mathematics: algebra, analysis, topology, number theory, measure theory, category theory, combinatorics, and more\n- **3,000+ stars** on GitHub, **34,000+ merged PRs**\n\nMathlib is the single largest factor in Lean's success. As Stephen Diehl writes: \"A theorem prover without a library is a programming language without packages. You can write everything from scratch, but you will not.\"\n\n### The Contribution Process\n\nFrom the [official contribution guide](https://leanprover-community.github.io/contribute/index.html) and the [Growing Mathlib paper](https://arxiv.org/abs/2508.21593) (Baanen et al., 2025):\n\n1. **Scope check**: Not everything belongs in Mathlib. Material should be \"typically taught or studied in a mathematics department.\" Contributors are encouraged to ask on the Lean Zulip `#mathlib` channel if uncertain.\n\n2. **Branch policy**: Contributors get push access to the mathlib4 repo (no forks needed). Create a branch, make changes, open a PR.\n\n3. **Style enforcement**: Mathlib has strict style guides covering naming conventions, documentation, code formatting, and mathematical generality. PRs must pass CI (continuous integration) which includes linting, compilation, and style checks.\n\n4. **Review**: PRs require review. **Reviewers do not have to be maintainers** — this is a common misconception. Contributors are encouraged to seek out reviewers. The review process is thorough but can be slow; as of September 2025, there were ~2,000 open PRs.\n\n5. **Delegation and merge**: Maintainers can \"delegate\" a PR (mark it as approved pending CI). Merging is handled by **Bors**, an automated merge bot that ensures the PR passes CI on the merge commit before actually merging.\n\n6. **AI use policy** (as of March 2026): AI-generated code is permitted but must be disclosed. Contributors must \"vouch for all code submitted\" and \"understand all content written by an AI.\" The guide explicitly warns: \"As of March 2026, AI-written code fails to meet [Mathlib's] bar by a large margin.\"\n\n### The \"Right Definitions\" Problem\n\nKevin Buzzard (Imperial College London) highlights that Mathlib's most important contribution is often **definitions**, not theorems. Getting the right definition — at the right level of generality, with the right interface — is an intensely collaborative process.\n\nFrom the Renaissance Philanthropy interview (Oct 2025):\n\n> \"One thing I've noticed is that we have a backlog of definitions. [...] I think Mathlib needs to have all standard modern definitions. I normally have a few missing definitions in mind at any given time. The examples I currently have are 'de Rham cohomology, symplectic manifolds, and Heegaard Floer homology.'\"\n\nThe community decides on definitions through Zulip discussion, experimentation in satellite projects, and review. Alex Kontorovich describes the workflow:\n\n> \"There's almost three skills. There's the skill of knowing the mathematics in the first place to write out a blueprint. There's a skill of coordinating people [...] to actually get it done. And then there's a really separate skill which is 'okay, now it's done, look back over this large 30,000-line project and figure out how to take little bits and pieces of it and get them into Mathlib.'\"\n\n### Dependency Structure and Maintenance\n\nThe \"Growing Mathlib\" paper (Baanen, Ballard, Commelin, Chen, Rothgang, Testa — 2025) addresses the maintenance challenges of a library this large:\n\n- **Dependency minimization**: PRs like `chore(Data/Nat/Factorization/Basic): minimize dependencies` are common — reducing import chains to keep compilation times manageable\n- **Refactoring at scale**: Operations like \"unbundle algebra from Seminormed groups\" touch hundreds of files and require careful coordination\n- **Bors queue management**: The CI pipeline must compile ALL of Mathlib for every merge, which takes significant compute\n- **The \"refactor tax\"**: When Lean itself changes (e.g., redefining `String`), Mathlib must adapt, sometimes requiring kernel-level coordination between the Lean team and Mathlib maintainers\n\n### The Mathlib Initiative\n\nIn late 2025, Renaissance Philanthropy launched the **Mathlib Initiative** with a donation from Alex Gerko (founder of XTX Markets), led by Johan Commelin, Oliver Nash, and Adam Topaz. The goal: professionalize Mathlib's infrastructure, increase review bandwidth, and fund targeted development in under-represented areas. The initiative represents a transition from purely volunteer-driven to professionally supported formalization.\n\n**Sources**: [Mathlib contribution guide](https://leanprover-community.github.io/contribute/index.html), [Renaissance Philanthropy interview](https://www.renaissancephilanthropy.org/insights/kevin-buzzard-and-alex-kontorovich-on-the-future-of-formal-mathematics-a-mathlib-initiative-interview), [Growing Mathlib (arXiv:2508.21593)](https://arxiv.org/abs/2508.21593)\n\n---\n\n## 5. What Made Lean 4 Succeed Where Others Didn't\n\n### Key Design Decisions\n\nFrom Stephen Diehl's \"From Zero to QED\" (2025) and cross-referencing multiple sources:\n\n**1. Speed**: Lean 4 compiles to C and runs fast. Not \"fast for a theorem prover\" — actually fast. You can write CLI tools, build systems, even games. IDE responsiveness determines whether people finish proofs or give up.\n\n**2. Metaprogramming in the same language**: Lean 4's tactic framework is written in Lean itself. In Coq, tactics use Ltac (a separate metalanguage). In Lean, tactics are just programs. You can inspect, modify, and write new tactics without learning a second language.\n\n**3. Syntax that looks like a normal programming language**: Functions are functions. Pattern matching works as expected. Unicode is optional. Lower friction = more users.\n\n**4. Mathlib as escape velocity**: Most theorem provers \"die the same death: they work, but nobody uses them.\" Mathlib provided the critical mass. \"When people ask 'can I formalize real mathematics?' the answer is: probably someone already did, go look it up.\"\n\n**5. Community momentum**: Kevin Buzzard teaching undergraduates at Imperial. Terence Tao formalizing his Analysis I textbook. The Lean Zulip is active and welcoming. When working mathematicians adopt your tool, the library grows faster.\n\n**6. AI integration**: Lean is the default target for neural theorem proving research. The metaprogramming API makes tool integration tractable. \"More AI tooling attracts more users attracts more AI tooling.\"\n\n### Comparison with Alternatives\n\n| Feature | Lean 4 | Coq/Rocq | Isabelle/HOL | Agda |\n|---------|--------|----------|--------------|------|\n| Type theory | CIC + quotients + choice | CIC | Higher-order logic (simpler) | Martin-Lof ITT |\n| Default logic | Classical | Constructive | Classical | Constructive |\n| Tactic language | Lean itself | Ltac (separate) | Isar (structured) | None (term-mode) |\n| Metaprogramming | In-language, first-class | OCaml plugins / Ltac2 | ML antiquotations | Reflection |\n| Math library | Mathlib (1.9M lines) | MathComp + others | AFP (large, fragmented) | ~none substantial |\n| IDE | VS Code (excellent) | VS Code (CoqLSP) | jEdit (proprietary) | Emacs (mainly) |\n| Programming | Full general-purpose | Limited extraction | Limited | Full |\n| Community hub | Zulip (very active) | Zulip + Discourse | Mailing list | Zulip |\n| AI research target | Primary | Secondary | Minimal | Minimal |\n\n### The Isabelle Perspective\n\nA revealing blog post from a 15-year Isabelle user (mrkeks.net, Dec 2025): When asked about VS Code/Copilot integration, an Isabelle core maintainer responded \"Oh dear, better use Lean then.\" The author reflects:\n\n> \"It seems that a maintainer writing a sentence like 'Better use [our competition] then!' has already given up the fight for his system to be the one that people will use in the next decade.\"\n\nIsabelle remains technically excellent (seL4 verified OS kernel was done in Isabelle) but has \"walled garden\" dynamics: no GitHub repo, special versioning system, \"giant barriers against drive-by pull requests.\"\n\n### The \"Formalisation Coefficient\"\n\nTerence Tao has spoken of a **formalisation coefficient**: the ratio of effort between writing a proof in Lean versus LaTeX. If this drops below 1, formalization becomes the default. Kontorovich draws the analogy to TeX adoption:\n\n> \"In '79 or '80, Knuth comes out with TeX and there's two people on planet Earth that use it. [...] But by the early 90s everybody [...] know how to use TeX. [...] The second that goes below one, everyone switches automatically.\"\n\nBuzzard is more cautious: \"I can't see the future. [...] it's not going to be in the next couple of years as far as I can see. I think a lot will depend on what AI can do.\"\n\n**Sources**: [From Zero to QED](https://sdiehl.github.io/zero-to-qed/03_theorem_provers.html), [Should I switch from Isabelle to Lean?](https://mrkeks.net/should-i-switch-from-isabelle-hol-to-lean/), [Renaissance Philanthropy interview](https://www.renaissancephilanthropy.org/insights/kevin-buzzard-and-alex-kontorovich-on-the-future-of-formal-mathematics-a-mathlib-initiative-interview)\n\n---\n\n## 6. The Proposer-Verifier Game: Lean + AI\n\n### The Architecture Pattern\n\nThe proposer-verifier pattern from AI safety states: if the verifier is trustworthy and the verification is cheap relative to generation, then the overall system is trustworthy regardless of how the proposer works. In Lean:\n\n- **Proposer**: Any system that generates proof terms or tactic sequences (human, LLM, RL agent, search algorithm)\n- **Verifier**: Lean's kernel (~5,000 lines of trusted C++ code)\n- **Verification cost**: Milliseconds to seconds (type-checking is decidable)\n- **Generation cost**: Seconds to hours (proof search is undecidable in general)\n\nThis asymmetry is what makes formal mathematics the \"killer app\" for AI verification. As the AlphaProof paper states:\n\n> \"Formal languages such as Lean offer an interactive environment that grounds reasoning [...] The soundness of this process is guaranteed by Lean's kernel, which verifies that the generated proof term is a valid construction.\"\n\n### AlphaProof (DeepMind, Nature 2025)\n\nAlphaProof is an AlphaZero-inspired agent that learns to find formal proofs through reinforcement learning. Key architectural elements:\n\n- **Training on auto-formalized problems**: Millions of informal math problems are translated to formal Lean statements, then used as training targets\n- **Test-time RL**: For difficult problems, AlphaProof generates and learns from millions of related problem *variants* at inference time — deep, problem-specific adaptation\n- **Lean as environment**: Mathematical reasoning is treated as an interactive game where the agent observes proof states, applies tactics, and receives feedback (proof accepted/rejected by kernel)\n\n**Results**: At the 2024 IMO, AlphaProof (combined with AlphaGeometry 2) solved 4 of 6 problems, achieving silver medal performance — the first AI system to reach medal-level at the IMO.\n\n**Critical limitation**: AlphaProof works within formal libraries. Many frontier research ideas aren't yet formalized. The **autoformalization bottleneck** — translating informal math (LaTeX, intuition) to formal statements — remains unsolved.\n\n### LeanDojo (Caltech/NVIDIA, NeurIPS 2023, v2 2025)\n\nLeanDojo is the infrastructure layer that makes AI+Lean research possible:\n\n1. **Repository tracing**: Automatically clones Lean repos and instruments them to extract theorem information, proof states, and structured training data\n2. **Gym-like environment**: Transforms Lean into an RL environment where AI agents can observe proof states, submit tactics, and receive feedback\n3. **ReProver**: A retrieval-augmented prover — given a proof state, it retrieves relevant premises from Mathlib, concatenates them with the state, and feeds everything into an encoder-decoder Transformer to predict the next tactic\n4. **Benchmarks**: LeanDojo Benchmark 4 contains 122,517 theorems, 259,580 tactics, and 167,779 premises from Mathlib4\n\nLeanDojo v2 (2025) adds:\n- **Lifelong dataset management**: Dynamic databases that append new theorems without retracing\n- **Multiple agent types**: Hugging Face fine-tuned models, external API agents, lifelong learning agents\n- **RL training**: GRPO (Group Relative Policy Optimization) for reinforcement learning\n- **Whole-proof generation**: Complete proofs in one forward pass, not just tactic-by-tactic\n\n### The Broader Landscape\n\nOther AI+Lean systems:\n- **DeepSeek-Prover**: Incentivizes reasoning in LLMs through RL, targeting Lean proofs\n- **UlamAI**: Open-source theorem prover formalized in Lean 4\n- **Pantograph**: Lean interaction server used by LeanDojo v2 for tactic-level proof search\n\nKevin Buzzard on AI's role (Oct 2025):\n\n> \"AI is doing the IMO and I imagine it's not going to stop there. [...] But I'm just coming to the conclusion now, that autoformalisation actually might be a much more viable idea. [...] You give it the system and it reads the paper and [...] it says 'I can put 90% of this together, but here are the 20 places where I couldn't follow.'\"\n\n**Sources**: [AlphaProof (Nature)](https://www.nature.com/articles/s41586-025-09833-y), [LeanDojo](https://leandojo.org/leandojo.html), [AlphaProof Explained](https://aidevelopercode.com/alphaproof-explained-what-googles-new-ai-mathematician-really-means-for-math)\n\n---\n\n## 7. Community Dynamics: The Lean Zulip\n\n### Structure\n\nThe Lean community operates primarily on **Zulip** (a threaded group chat, similar to Slack but with proper topic threading). Key streams:\n\n- `#general`: Announcements, broad discussions\n- `#new members`: Onboarding, beginner questions (very active, welcoming)\n- `#mathlib4`: Mathlib-specific development discussion\n- `#maths`: Mathematical questions about formalization strategy\n- `#lean4`: Language-level questions and issues\n- `#Is there code for X?`: Checking whether something already exists in Mathlib\n\nThe threading model is important: unlike Slack/Discord, Zulip topics don't get lost. The entire archive is [publicly searchable](https://leanprover-community.github.io/archive/). This creates institutional memory.\n\n### Collaboration Patterns\n\nFrom observation of the contribution workflow and the Buzzard/Kontorovich interviews:\n\n1. **Blueprint-driven projects**: Large formalizations (Fermat's Last Theorem, Prime Number Theorem) use \"blueprints\" — structured dependency graphs of lemmas needed, with each node marked as formalized or not. Community members can pick up individual nodes.\n\n2. **Symbiotic relationship with Mathlib**: Research projects depend on Mathlib but also produce results that should flow back. This creates a two-way tension — projects want to move fast (no review overhead), but the community wants results to be properly generalized and integrated.\n\n3. **The \"three skills\" model** (Kontorovich): Knowing the mathematics, coordinating the formalization, and refactoring results into Mathlib-quality contributions are distinct skills that different people may excel at.\n\n4. **Teaching as onramp**: Buzzard's undergraduate course at Imperial, Tao's Analysis I companion, and the \"Natural Number Game\" serve as entry points. Kontorovich's dream: \"eventually every undergraduate subject is just a game and a 12-year-old can learn the entire undergraduate curriculum formally.\"\n\n---\n\n## 8. Progressive Formalization: From Intuition to Machine-Checked Proof\n\n### Terence Tao's Approach\n\nTao's [Lean companion to Analysis I](https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/) (May 2025) demonstrates progressive formalization:\n\n1. **Build from scratch, then connect to Mathlib**: The formalization first develops `Chapter2.Nat` (natural numbers) \"by hand\" as exercises, paralleling the textbook. Then an epilogue establishes isomorphisms with Mathlib's standard natural numbers. From that point on, the custom definitions are deprecated and Mathlib's are used.\n\n2. **\"Sorry\"-driven development**: Theorems are stated with `sorry` (unproven placeholder) and students fill them in. The code compiles (with warnings) regardless of whether the exercises are solved.\n\n3. **Deliberate separation then integration**: \"As one advances into later chapters, one increasingly relies on Mathlib's definitions and functions, rather than directly referring to any counterparts from earlier chapters.\"\n\nTao notes:\n\n> \"The 'naive type theory' that I was implicitly using to do things like construct the standard number systems, dovetails well with the dependent type theory of Lean (which, among other things, has excellent support for quotient types).\"\n\n### The General Workflow\n\nFor working mathematicians formalizing new results:\n\n1. **Write a LaTeX proof** (informal, standard mathematical practice)\n2. **Create a blueprint**: Decompose into lemmas with dependency structure\n3. **State theorems in Lean**: Often the hardest part — choosing the right types, finding the right Mathlib abstractions\n4. **Prove interactively**: Using tactics, consulting Mathlib (via `exact?`, `apply?`, `search_lemma` tactics), asking on Zulip\n5. **Refactor for Mathlib submission**: Generalize, match Mathlib style, minimize dependencies\n\nThe bottleneck is almost always step 3 — **stating theorems correctly** requires understanding both the mathematics AND the library's conventions. This is the autoformalization problem.\n\n---\n\n## 9. Type Classes, Structures, and Definitions\n\n### Structures\n\nStructures in Lean are inductive types with a single constructor. They define bundled data with named fields:\n\n```lean\nstructure Semigroup :=\n  (Carrier : Type)\n  (mul : Carrier -> Carrier -> Carrier)\n  (mul_assoc : forall a b c, mul (mul a b) c = mul a (mul b c))\n```\n\n### Type Classes\n\nLean uses **type classes** (borrowed from Haskell, extended for dependent types) to handle algebraic hierarchies. A type class is a structure marked with `class`, and instances are registered with `instance`:\n\n```lean\nclass Add (a : Type) where\n  add : a -> a -> a\n\ninstance : Add Nat where\n  add := Nat.add\n```\n\nThe elaborator uses **type class inference** (a Prolog-like search) to automatically find instances. This is how `+` works on different types without explicit annotation.\n\nMathlib's algebraic hierarchy is built on type classes: `Monoid`, `Group`, `Ring`, `Field`, `TopologicalSpace`, `MetricSpace`, etc. The hierarchy is carefully designed so that instances compose — if `R` is a `CommRing` and an `Algebra` over a field `k`, then it automatically gets all the structure of both.\n\n### The Definitional Equality Design Space\n\nLean makes careful choices about what counts as definitionally equal:\n- **Proof irrelevance**: Any two proofs of the same proposition in `Prop` are definitionally equal. This is key — you never need to prove that two proofs are \"the same proof.\"\n- **Quotient types**: Built into the kernel (not derived from other axioms). This gives function extensionality and enables clean handling of equivalence classes.\n- **No unification hints**: Unlike Coq's canonical structures, Lean relies primarily on type class inference. This is simpler but sometimes less powerful for specific patterns.\n\n---\n\n## 10. Relevance to Deliberus\n\n### Direct Architectural Parallels\n\nThe Lean kernel architecture maps directly to Deliberus's design space:\n\n| Lean Concept | Deliberus Analog |\n|-------------|-----------------|\n| Trusted kernel (small, auditable verifier) | Logical kernel for argument validity checking |\n| Elaboration layer (user-facing to kernel-internal) | Translation from natural language claims to formal argument structure |\n| Tactics (human-guided, machine-checked proof construction) | Guided claim decomposition and evidence linking |\n| Mathlib (community-built library of verified results) | Community-built library of vetted arguments and evidence |\n| Proof terms (the ground truth artifact) | Formal argument graphs (the ground truth artifact) |\n| Type class inference (automatic structure discovery) | Automatic classification of claim types and relationships |\n\n### The Proposer-Verifier Pattern for Arguments\n\nLean demonstrates that the proposer-verifier separation works at civilizational scale:\n- The \"proposer\" can be creative, messy, AI-assisted, or human\n- The \"verifier\" is small, auditable, and trustworthy\n- The resulting artifacts (proofs/arguments) are trustworthy regardless of how they were constructed\n\nFor Deliberus, this suggests: invest heavily in the verification layer (argument validity kernel), and allow maximum creativity in the construction layer (how people formulate and submit arguments).\n\n### The Formalisation Coefficient for Arguments\n\nTao's \"formalisation coefficient\" concept applies directly: the ratio of effort to formally structure an argument versus stating it informally. If Deliberus can get this ratio close to 1 (through AI assistance, good UX, progressive formalization workflows), adoption becomes natural.\n\n### The Library Problem\n\nLean's success hinged on Mathlib — having a critical mass of formalized mathematics that new work could build on. Deliberus faces the same challenge: the platform needs a critical mass of structured arguments before it becomes self-sustaining. The \"escape velocity\" problem is real.\n\n### Progressive Formalization as UX Pattern\n\nTao's approach — start informal, gradually formalize, connect to the shared library — is a template for Deliberus UX. Users should be able to:\n1. State claims informally\n2. Gradually structure them (identify premises, distinguish normative from descriptive)\n3. Connect to the shared argument graph\n4. Get \"credit\" for partially-formalized contributions (like `sorry` in Lean)\n\n---\n\n## Key Sources\n\n1. **Avigad, J.** Lecture notes on dependent type theory and Lean's formal foundation. Hausdorff School, 2023. [Gist](https://gist.github.com/avigad/1316b67a27fab2865cf8ef3993fd5e27)\n2. **Diehl, S.** \"From Zero to QED: Theorem Provers.\" 2025. [Link](https://sdiehl.github.io/zero-to-qed/03_theorem_provers.html)\n3. **Buzzard, K. & Kontorovich, A.** Renaissance Philanthropy interview on Mathlib Initiative. Oct 2025. [Link](https://www.renaissancephilanthropy.org/insights/kevin-buzzard-and-alex-kontorovich-on-the-future-of-formal-mathematics-a-mathlib-initiative-interview)\n4. **AlphaProof team (DeepMind).** \"Olympiad-level formal mathematical reasoning with reinforcement learning.\" Nature, Nov 2025. [Link](https://www.nature.com/articles/s41586-025-09833-y)\n5. **Yang, K. et al.** \"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models.\" NeurIPS 2023. [Link](https://leandojo.org/leandojo.html)\n6. **Tao, T.** \"A Lean companion to Analysis I.\" May 2025. [Link](https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/)\n7. **Baanen, A. et al.** \"Growing Mathlib: maintenance of a large scale mathematical library.\" 2025. [arXiv:2508.21593](https://arxiv.org/abs/2508.21593)\n8. **Lean Community.** \"Metaprogramming in Lean 4.\" [Link](https://leanprover-community.github.io/lean4-metaprogramming-book/)\n9. **Lean Community.** \"How to contribute to Mathlib.\" [Link](https://leanprover-community.github.io/contribute/index.html)\n10. **Lean Community.** \"Theorem Proving in Lean 4.\" [Link](https://lean-lang.org/theorem_proving_in_lean4/)\n11. **mrkeks.** \"Should I switch from Isabelle/HOL to Lean?\" Dec 2025. [Link](https://mrkeks.net/should-i-switch-from-isabelle-hol-to-lean/)\n"}