{"path":"research/lean-social-system-research.md","content":"# Lean Proof Assistant as a Social System: Research for Deliberus Analogies\n\n**Date**: 2026-03-28\n**Purpose**: Understanding how Lean's community mechanisms work as a *social* system, to inform Deliberus's collaborative deliberation platform design.\n\n---\n\n## 1. The `sorry` Mechanism: Structured Incompleteness\n\n### How It Works\n\n`sorry` is a built-in axiom in Lean that can prove *any* proposition. It is Lean's placeholder for unproven lemmas, allowing you to sketch the structure of a proof before filling in every detail.\n\n```lean\ntheorem pfr : ... := by\n  sorry  -- proof not yet provided\n```\n\nWhen you use `sorry`, the code compiles — but Lean marks everything that depends on it with a warning. The compiler tracks `sorry` transitively: if theorem B depends on theorem A, and A uses `sorry`, both are flagged. This creates a clear audit trail of what is truly proven vs. what is sketched.\n\nCritically, `sorry` makes the proof system **unsound** — it can prove `False`. A completed proof is one with *zero* `sorry` instances. The compiler explicitly warns about `sorry` usage, making incompleteness visible rather than hidden.\n\n### Social Dynamics\n\nFrom Terence Tao's PFR project blog post (Nov 2023): contributors could work on individual lemmas by \"filling in the `sorry`s\" without understanding the entire proof. The project's dependency graph showed which bubbles were green (fully proven), blue (statement formalized, ready to prove), or white (not yet formalized). This visual map let 25+ contributors self-organize: pick a blue bubble, fill in its `sorry`, submit a PR.\n\nKey quote from Tao: \"One key advantage of working with a project based around a proof assistant language such as Lean is that it makes large-scale mathematical collaboration possible without necessarily having a pre-established level of trust amongst the collaborators; my fellow repository maintainers and I have already approved several pull requests from contributors that had not previously met, as the code was verified to be correct.\"\n\n### Deliberus Analogy\n\n`sorry` is the proof-world equivalent of marking an argument node as \"placeholder — reasoning needed here.\" A deliberation platform could allow users to sketch the *structure* of an argument (claim + subclaims + needed evidence) with explicit \"sorry\" markers where reasoning is incomplete. This enables:\n- **Structural sketching before detail**: Map the argument landscape, fill in rigor later\n- **Trustless collaboration**: Anyone can contribute a sub-argument; the system verifies it fits\n- **Visible incompleteness**: The platform shows exactly what's proven and what's placeholder\n- **Parallel work**: Different contributors fill in different `sorry` nodes independently\n\n---\n\n## 2. Refactoring Mathematical Foundations\n\n### The Process\n\nThe paper \"Growing Mathlib\" (Baanen et al., 2025, arXiv:2508.21593) describes how Mathlib handles changing definitions — a process that is *exceedingly common*:\n\n> \"Generalizations, refactors, reorganization of content, syntax changes and so on are exceedingly common in Mathlib. As a result, code written for one version of Mathlib may no longer compile with a newer version.\"\n\nMathlib uses a formal **deprecation system** for managing change:\n\n1. **Grace period**: When a declaration is renamed or redefined, a deprecation marker connects old and new names for several months. Users see a warning but code still works.\n\n2. **Linters enforce quality**: Two linter frameworks (syntax linters for immediate feedback, environment linters for global validation) automatically check that contributions meet standards — naming conventions, style, proper attributes, etc.\n\n3. **Breaking changes are managed socially**: Proposed changes are discussed on the Lean Zulip chat. Major refactors require RFC (Request for Comments) issues on GitHub. The community debates whether the new definition is \"better\" — often a surprisingly philosophical question.\n\n4. **Incremental migration**: Rather than a big-bang switch, the old and new definitions coexist during a transition period. Automated tools (meta-programs) can often handle mechanical migration.\n\n### Real Examples\n\n- `LinearIndependent` was refactored to use `LinearIndepOn` (PR #21886) — fundamentally changing how linear independence is expressed\n- The entire Lean 3 to Lean 4 port (completed July 2023) was a massive community effort to migrate the entire mathematical library to a new language version\n- Definition quality is reviewed extremely carefully: \"if you miss or garble an axiom then your code will still compile, it just won't mean what it is supposed to mean\" (Kevin Buzzard, Feb 2026)\n\n### The Governance\n\nFrom the PR Review Guide: \"Mathlib maintainers are the only users with authority to merge pull requests, everyone is welcome, and even encouraged, to review pull requests.\" There is also a \"mathlib reviewer\" tier — people who have demonstrated consistent high-quality reviews. This creates a three-tier system: contributor > reviewer > maintainer.\n\nCode review in Mathlib is **decentralized**: everybody can review, and the approval system is multi-stage. The recently created **Mathlib Initiative** (funded) pays expert humans to review PRs, addressing a backlog that reached 2000+ open PRs.\n\n### Deliberus Analogy\n\nThis maps directly to how a deliberation platform might handle \"refactoring\" of foundational claims:\n- **Deprecation system**: When a better formulation of a claim is found, the old one isn't deleted — it's linked to the new formulation with a transition period\n- **Linters for arguments**: Automated checks for logical structure, missing premises, unsupported claims\n- **Social governance of definitions**: The community debates what counts as the \"canonical\" formulation of a contested concept — exactly the kind of deliberation Deliberus is meant to support\n- **Incremental migration**: Old argument structures coexist with new ones during transition, preventing disruption\n\n---\n\n## 3. The Blueprint System\n\n### What It Is\n\nLean Blueprint (created by Patrick Massot, 2020; GitHub: PatrickMassot/leanblueprint, 317 stars) is a tool for writing human-readable proof plans that get progressively formalized into verified Lean code. It was originally created for the **Sphere Eversion Project** and has since been used by 40+ major formalization projects.\n\n### How It Works\n\n1. **Write LaTeX**: Authors write a conventional mathematical proof in LaTeX, broken into labeled lemmas and definitions\n2. **Add Lean links**: Each lemma/definition gets linked to its Lean formalization (or marked as \"not yet formalized\")\n3. **Generate dependency graph**: The tool automatically creates a visual graph showing how lemmas depend on each other\n4. **Color-coded status**:\n   - **Green**: Fully formalized (both statement and proof in Lean)\n   - **Blue**: Statement formalized, proof ready to be written (all prerequisites done)\n   - **White with green border**: Statement formalized, but some prerequisites missing\n   - **Orange**: Far from being formalizable (many dependencies unmet)\n5. **Progressive formalization**: The graph evolves from mostly white/orange to green as contributors work in parallel\n\n### The PFR Success Story\n\nTao's PFR project (Nov 2023) demonstrated the blueprint at scale: a 33-page paper was formalized in three weeks by 25 contributors. The blueprint enabled:\n- **Self-organization**: Contributors could see which lemmas were \"blue\" (ready to work on) and pick tasks\n- **Parallel work without coordination overhead**: No need to understand the entire proof — just your lemma and its immediate dependencies\n- **Dual readability**: The same document was comprehensible to both humans (LaTeX) and machines (Lean)\n- **Progress visibility**: The dependency graph was a live dashboard of the project's state\n\n### Notable Projects Using Blueprint\n\n- Sphere eversion, Liquid tensor experiment, PFR conjecture, Fermat's Last Theorem (ongoing), Carleson operators, Equational theories, Semi-circle law, Brownian motion formalization, and 30+ more\n\n### Deliberus Analogy\n\nThe blueprint is perhaps the *most directly relevant* Lean concept for Deliberus:\n- **Argument blueprints**: Users write a human-readable argument structure (like the LaTeX blueprint) that gets progressively verified/supported\n- **Dependency graphs of reasoning**: Claims depend on sub-claims, evidence, and definitions — the graph shows what's supported and what's not\n- **Color-coded argument health**: Green = well-supported, blue = ready for evidence, orange = far from resolved\n- **Parallel contribution**: Different people can strengthen different parts of the argument independently\n- **Dual readability**: The same argument structure is accessible at the human-language level and the formal-logic level\n\n---\n\n## 4. Type Class Inference as Knowledge Graph\n\n### How It Works\n\nLean's type class system is a **recursive search procedure** that automatically resolves chains of mathematical structure. When you write code that needs, say, addition on a type, Lean automatically searches through a hierarchy of instances to find one that applies.\n\nFrom the official Lean reference: \"Instance synthesis is a recursive search procedure that either finds an instance for a given type class or fails. Given a type that is registered as a type class, instance synthesis attempts to construct a term with said type.\"\n\nThe key properties:\n- **Diamond-safe**: Multiple paths to the same goal are handled efficiently via tabling (memoization)\n- **Cycle-safe**: Mutual dependencies between instances don't cause infinite loops\n- **Priority-ordered**: When multiple instances match, declared priorities and recency determine which is chosen\n- **Input/output parameters**: Some parameters drive the search (inputs), others are determined by it (outputs)\n\n### The Resolution Chain\n\nConsider the mathematical hierarchy: a field is a ring, a ring has addition, addition means it's an additive group, etc. When you use `+` on elements of a field, Lean automatically resolves:\n\n```\nField → CommRing → Ring → AddCommGroup → AddGroup → AddMonoid → Add\n```\n\nThis chain is traversed **automatically** — the user writes `a + b` and Lean figures out which addition to use based on the type. Each step in the chain is an instance, and the collection of all instances forms an implicit **knowledge graph** of mathematical structure.\n\n### Social Dynamics\n\nThe \"Use and Abuse of Instance Parameters in the Lean Mathematical Library\" (Baanen, ITP 2022) analyzes how this system works in practice. Key challenges:\n- **Diamond problem**: When there are multiple paths to the same instance, they must agree (be \"definitionally equal\") — otherwise the system breaks\n- **Performance**: Deep instance chains slow down compilation. The community carefully designs hierarchies to minimize search depth\n- **\"Morally canonical\" instances**: Lean assumes that if two instances exist for the same class, they should be interchangeable — this is a *social contract* among library contributors\n\n### Deliberus Analogy\n\nType class inference is analogous to **navigating a web of interconnected concepts**:\n- **Implicit resolution**: When someone makes a claim about \"fairness,\" the system could automatically resolve what framework of fairness they're using (based on context)\n- **Diamond handling**: When two reasoning paths lead to the same conclusion via different routes, the system must handle this gracefully\n- **Priority and recency**: More specific or more recent formulations take precedence — like how recent evidence supersedes older evidence\n- **The knowledge graph IS the hierarchy**: The entire mathematical hierarchy is encoded as instances — this is literally a knowledge graph traversed by automated search\n\n---\n\n## 5. Simp Lemmas: A Growing Automated Knowledge Base\n\n### How It Works\n\nThe `simp` tactic (simplifier) is Lean's primary tool for automated rewriting. It works by applying a set of rewrite rules (called a \"simp set\") to simplify expressions. The crucial mechanism: any lemma tagged with `@[simp]` is automatically added to the default simp set.\n\nFrom the Lean reference on simp sets: \"A collection of rules used by the simplifier is called a simp set. A simp set is specified in terms of modifications from a default simp set. These modifications can include adding rules, removing rules, or adding a set of rules.\"\n\n### The Growing Knowledge Base\n\nEvery time a contributor proves a new lemma and tags it `@[simp]`, the system gets slightly smarter:\n- `@[simp]` lemmas accumulate across the entire library\n- The `simp` tactic can close goals that require combining multiple lemmas\n- Mathlib's `@[simps]` attribute auto-generates simp lemmas for new definitions\n\nThe PR Review Guide specifically asks reviewers: \"are lemmas tagged `@[simp]`, `@[ext]`, et cetera where they should be? or shouldn't be?\" This is a governance question — tagging a lemma as `@[simp]` changes the behavior of *every future proof* that uses `simp`.\n\n### Quality Control\n\nNot every true equation should be a simp lemma. The community maintains norms about what makes a good simp lemma:\n- Should simplify (reduce complexity, not increase it)\n- Should be confluent (order of application shouldn't matter)\n- Should not loop (combining two simp lemmas shouldn't cycle)\n- Should terminate\n\nThese norms are enforced by code review and linters.\n\n### Deliberus Analogy\n\nThe simp system embodies **accumulated community knowledge that automates reasoning**:\n- **Crowdsourced simplification rules**: Each verified argument adds to the platform's ability to automatically simplify future arguments\n- **Quality gates on automation**: Not every proven claim should be in the auto-reasoning set — the community curates what's \"safe\" to use automatically\n- **Growing competence**: The more the community contributes, the more the system can do automatically — this is the \"flywheel\" effect\n- **Tagged knowledge**: Claims tagged as \"self-evident\" or \"foundational\" can be used automatically; others require explicit invocation\n\n---\n\n## 6. The Buzzard/Tao Effect\n\n### Kevin Buzzard's Role\n\nKevin Buzzard, a number theorist at Imperial College London, became the most visible evangelist for Lean in mathematics. His **Xena Project** (blog: xenaproject.wordpress.com) trained undergraduates in formalization, and his talks (\"The Future of Mathematics?\") challenged the mathematical community's complacency about proof correctness.\n\nKey contributions:\n- **Made Lean accessible to mathematicians**: His teaching materials and blog posts bridge the gap between type theory and mathematical practice\n- **Credibility transfer**: As a respected number theorist, his endorsement gave Lean legitimacy among working mathematicians\n- **Ambitious projects**: His 5-year EPSRC-funded project to formalize Fermat's Last Theorem (announced 2024) demonstrated that Lean could handle deep modern mathematics\n- **Honest criticism**: His Feb 2026 post \"Accelerating Mathematics\" was bluntly honest about LLMs' limitations and the difficulty of scaling formalization\n\nBuzzard's key insight (Feb 2026): \"LLMs will lie to you. I've asked a language model a question and have been unambiguously told that the answer is YES and given a 'proof' which, when inspected turns out to be nonsense.\" This is the motivating problem that formal verification addresses — and that Deliberus addresses for informal argumentation.\n\n### Terence Tao's Impact\n\nTao, arguably the world's most prominent living mathematician, began using Lean in 2023 with the PFR project. His adoption had immediate effects:\n- **25 contributors** assembled within days for the PFR formalization\n- His detailed blog post (Nov 2023) became the canonical introduction to collaborative Lean projects\n- He demonstrated that formalization could happen in \"real time\" — the proof was formalized faster than it was refereed\n- His \"Lean phrasebook\" connecting mathematical English to Lean tactics became a widely-used resource\n- He tracks AI+math developments (LLM/Lean combos solving Erdos problems)\n\n### What Made Lean Compelling\n\nFrom Buzzard's \"Lean in 2024\" post:\n1. **Mathlib's growth**: \"a very fast-growing database of mathematics\" reaching critical mass\n2. **Real-time formalization**: Multiple breakthrough results (PFR, Ramsey bounds, Erdos-Graham) formalized before or shortly after peer review\n3. **The Lean FRO** (Focused Research Organization): Funded by Simons Foundation, Sloan, and Richard Merkin — full-time infrastructure team\n4. **Practical tools**: `omega` tactic for integer arithmetic, LeanCopilot for AI-assisted proving, widgets for interactive visualization\n5. **Community infrastructure**: Zulip chat, PR review system, Natural Number Game for beginners\n\n### Deliberus Analogy\n\nThe Buzzard/Tao effect demonstrates **how champion adoption transforms a community**:\n- **Credibility transfer**: When respected domain experts endorse a tool, the entire field pays attention\n- **Proof by example**: Tao didn't argue for formalization in the abstract — he formalized his own breakthrough result\n- **Honest assessment of limitations**: Buzzard's frank assessment of what Lean can't do builds trust more than overselling\n- **The \"LLMs lie\" problem**: This is exactly the problem Deliberus addresses — how do you distinguish genuine reasoning from plausible-sounding nonsense? Lean's answer: formal verification. Deliberus's answer: structured argumentation with community vetting.\n\n---\n\n## 7. Handling Disagreements About Formalization Choices\n\n### The Process\n\nFrom the \"Growing Mathlib\" paper and PR Review Guide:\n\n1. **Zulip discussion first**: Major design decisions are debated on the Lean Zulip chat before code is written. This is the equivalent of an RFC process.\n\n2. **PR review as deliberation**: The review guide asks: \"are the definitions introduced the best way to formalize the concept (very difficult!)?\" This is explicitly acknowledged as the hardest review question.\n\n3. **Principle: avoid dependent types when possible**: \"the more definitions avoid dependent types, the better\" — this is a community-evolved heuristic, not a formal rule.\n\n4. **Definition quality is paramount**: Buzzard (Feb 2026): \"if you miss or garble an axiom then your code will still compile, it just won't mean what it is supposed to mean.\" Proofs are machine-checked; *definitions* require human judgment.\n\n5. **Multi-stage approval**: contributor → reviewer → maintainer, with each tier having different authority. Reviewers can approve, but only maintainers can merge. The `bors` bot enforces this.\n\n6. **\"Does it fit the design and collective vision of mathlib?\"**: The review guide explicitly asks this — meaning there IS a collective vision, maintained socially through norms rather than formal rules.\n\n### Resolution Mechanisms\n\n- **Generality wins**: If two formalizations disagree, the more general one usually wins — the one that applies to more cases\n- **API quality matters**: A definition is judged by the lemmas it enables. If one formalization leads to cleaner downstream proofs, it wins\n- **Deprecation over deletion**: The old formalization gets deprecated, not immediately removed\n- **Authority structure**: Maintainers have final say, but they exercise it rarely and with deference to domain experts\n- **\"Library integration\" review**: New code is judged on whether it \"advances or improves the library\" as a whole — not just whether it's correct\n\n### Deliberus Analogy\n\nThis is the **core governance question** for any collaborative knowledge system:\n- **Discussion before formalization**: Deliberate about the *structure* of an argument before committing to a specific formulation\n- **Multi-tier review**: Different roles have different authority — contributors propose, reviewers validate, maintainers adjudicate\n- **Generality as tie-breaker**: When two formulations of a claim compete, prefer the one that connects to more reasoning\n- **The definition problem**: In argumentation, defining terms precisely is as hard as it is in mathematics — and just as critical\n- **Collective vision maintenance**: The community's norms are maintained through social processes (discussion, review, teaching), not just rules\n\n---\n\n## 8. Automation Tactics: Accumulated Mathematical Knowledge\n\n### The Taxonomy\n\nLean's automation tactics embody different forms of accumulated knowledge:\n\n| Tactic | What It Knows | How It Works |\n|--------|--------------|--------------|\n| `omega` | Linear integer arithmetic | Implements William Pugh's omega test algorithm — a *complete* decision procedure for Presburger arithmetic |\n| `decide` | Decidable propositions | Computes whether something is true by exhaustive evaluation |\n| `norm_num` | Numerical normalization | Extensible plugin system; registered `@[norm_num]` extensions teach it new normalizations |\n| `simp` | Rewrite rules | Applies tagged `@[simp]` lemmas — grows with every new contribution |\n| `linarith` | Linear arithmetic over ordered fields | Proves goals derivable by linear combinations of hypotheses |\n| `polyrith` | Polynomial arithmetic | *Was* backed by external Sage server (now shut down); replaced by `grobner` tactic |\n| `positivity` | Positivity of expressions | Proves `0 < expr` or `0 ≤ expr` from structure |\n| `gcongr` | Monotonicity/congruence | Applies congruence lemmas for inequalities |\n| `aesop` | General-purpose search | Configurable rule-based proof search, like an extensible auto |\n| `exact?` / `apply?` | Library search | Searches the entire library for a lemma matching the goal |\n\n### Two Modes of Knowledge\n\n1. **Algorithmic knowledge** (`omega`, `decide`, `norm_num`): These encode *mathematical algorithms* — decision procedures that are provably complete for their domain. They don't grow with the library; they embody fixed mathematical knowledge.\n\n2. **Accumulated knowledge** (`simp`, `aesop`, `exact?`): These grow with every contribution. Each `@[simp]` lemma, each `@[aesop]` rule, each new library lemma makes these tactics more powerful. This is **crowdsourced automation**.\n\n### Social Dynamics\n\nFrom Tao's PFR tour: he used `linarith` (solved a linear arithmetic step automatically), `exact?` (searched the library and found the right lemma), and GitHub Copilot (AI suggestion, \"almost correct\"). The layering is: human strategy + tactic automation + AI suggestion.\n\nThe FRO (Lean Focused Research Organization) develops tactics like `omega` to make common proof steps trivial. Scott Morrison's `omega` for Lean 4 specifically aimed to prevent undergraduate students from getting stuck on \"obvious\" integer lemmas.\n\n### Deliberus Analogy\n\nThis maps to **automated reasoning layers** in a deliberation platform:\n- **Algorithmic layer**: Logic checkers, consistency validators, deductive closure — these are fixed algorithms that check argument structure\n- **Accumulated layer**: The more the community proves, the more the system can auto-verify. \"This claim follows from established claims X, Y, Z\" — the system searches for this automatically\n- **Library search**: \"Has someone already addressed this argument?\" — searching the existing knowledge base for relevant prior reasoning\n- **The `exact?` moment**: The system suggests \"this claim is exactly what was proven in discussion #4523\" — connecting new arguments to existing verified ones\n\n---\n\n## 9. Lake Build System and Project Management\n\n### How Lake Works\n\nLake (Lean Make) is Lean's build system and package manager. It manages:\n\n- **Dependencies**: Projects declare dependencies on other packages (most importantly Mathlib). Lake fetches them from Git repositories.\n- **Incremental builds**: Only recompiles files that changed or whose dependencies changed. Essential because Mathlib alone takes 30+ minutes to compile from scratch.\n- **Configuration**: Written in Lean itself (or TOML), meaning the build configuration is type-checked.\n- **Reservoir integration**: Connects to Reservoir, Lean's package server — a registry of available packages.\n\n### Incremental Compilation is Critical\n\nMathlib is 1.9 million lines of code. Without incremental builds, every change would require recompiling everything. Lake tracks dependencies at the file level and recompiles only what's necessary. The community is very conscious of **import hierarchies** — adding an unnecessary import can cause huge compilation cascades.\n\nFrom the PR Review Guide: \"Are new imports introduced, and if so, do they import too much material for this file?\" and \"Should some of the results be placed into a new file to minimize import requirements?\"\n\nThis is a **graph optimization problem**: minimize the dependency graph's depth and breadth to minimize compilation time. The community actively refactors the import hierarchy for performance.\n\n### Project Structure for Large Formalizations\n\nLarge projects (PFR, Fermat's Last Theorem) depend on Mathlib and are managed as separate Lake projects. Contributors:\n1. Clone the repo\n2. `lake build` fetches dependencies and builds\n3. Work on their piece\n4. Submit a PR\n5. CI runs `lake build` to verify the entire project still compiles\n\n### Deliberus Analogy\n\nLake's approach to managing large interconnected knowledge bases applies to:\n- **Incremental validation**: When a claim is updated, only re-check the arguments that depend on it — not the entire knowledge base\n- **Dependency management**: Arguments depend on other arguments, definitions, and evidence sources. Track these dependencies explicitly.\n- **Import hierarchy as argument topology**: The structure of which files import which in Mathlib mirrors how argument modules would reference each other\n- **Compilation time as user experience**: If re-validating an argument change takes too long, the platform becomes unusable. Incremental re-validation is essential.\n\n---\n\n## Cross-Cutting Themes for Deliberus\n\n### 1. Trustless Collaboration Through Formal Verification\n\nLean's deepest social innovation: strangers can contribute to a shared proof without trusting each other, because the compiler verifies correctness. Deliberus needs an analogous mechanism for argumentation — not full formal verification (arguments are richer than proofs), but structural validation that a contribution fits the expected pattern.\n\n### 2. The Definition Problem\n\nBoth Lean and Deliberus face the same fundamental challenge: definitions are uncheckable by machine. Lean's compiler can verify that a proof is valid *given* the definitions, but cannot check that the definitions capture the intended mathematical concept. Similarly, a deliberation platform can check argument structure, but whether the concepts are defined accurately is a human judgment call. This is why both systems invest so heavily in social review processes around definitions.\n\n### 3. Progressive Formalization via Blueprints\n\nThe blueprint pattern — human-readable structure linked to progressively formalized content — is the single most transferable concept. An argument blueprint would show: the overall structure, what's been verified, what needs work, and how to contribute.\n\n### 4. Accumulated Knowledge Creates Automation\n\nEvery `@[simp]` lemma makes Lean smarter. Every verified argument in Deliberus should make the platform better at recognizing and connecting related claims. The flywheel effect: community contribution grows system capability, which attracts more contribution.\n\n### 5. Honest Assessment of Limitations\n\nBuzzard's frank admission that \"LLMs will lie to you\" and his honest assessment of what Lean can and cannot do (Feb 2026) builds more trust than overselling. A deliberation platform should be equally honest about what it can and cannot verify.\n\n### 6. The Community IS the System\n\nMathlib's governance — Zulip discussions, multi-tier review, collective vision, deprecation processes — is as much a part of the \"proof assistant\" as the software. The social norms ARE the quality control. Deliberus should design its social processes with the same intentionality that Lean designs its type system.\n\n---\n\n## Sources\n\n### Primary Sources (Crawled)\n- Terence Tao, \"Formalizing the proof of PFR in Lean4 using Blueprint: a short tour\" (Nov 2023): https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/\n- Kevin Buzzard, \"Accelerating Mathematics\" (Feb 2026): https://xenaproject.wordpress.com/2026/02/09/accelerating-mathematics/\n- Kevin Buzzard, \"Lean in 2024\" (Jan 2024): https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/\n- Baanen et al., \"Growing Mathlib: maintenance of a large scale mathematical library\" (2025): https://arxiv.org/html/2508.21593v2\n- Mathlib PR Review Guide: https://leanprover-community.github.io/contribute/pr-review.html\n- Lean Reference: Instance Synthesis: https://lean-lang.org/doc/reference/4.22.0-rc4/Type-Classes/Instance-Synthesis/\n- Lean Reference: Simp Sets: https://lean-lang.org/doc/reference/4.20.0-rc2/The-Simplifier/Simp-sets/\n- Patrick Massot, leanblueprint (GitHub): https://github.com/PatrickMassot/leanblueprint\n\n### Secondary Sources (Search Results)\n- Lean Reference: Type Classes: https://lean-lang.org/theorem_proving_in_lean4/Type-Classes/\n- Lean Reference: Lake: https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/\n- Lean omega tactic: https://lean-lang.org/doc/api/Lean/Elab/Tactic/Omega.html\n- Lean decide tactic: https://lean4.dev/tactics/automation/decide\n- Mathlib polyrith: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Polyrith.html\n- Mathlib norm_num: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/NormNum/Core.html\n- Kevin Buzzard, \"The Future of Mathematics?\" (MSR talk, 2019): https://www.ma.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf\n- Kevin Buzzard, \"The Fermat's Last Theorem Project\" (2024): https://leanprover-community.github.io/blog/posts/FLT-announcement/\n- Baanen, \"Use and Abuse of Instance Parameters in the Lean Mathematical Library\" (ITP 2022)\n- van Doorn, Ebner, Lewis, \"Maintaining a Library of Formal Mathematics\": https://florisvandoorn.com/papers/maintenance.pdf\n- lean-graph (theorem dependency visualization): https://github.com/patrik-cihal/lean-graph\n- Lean Zulip Chat Archive: https://leanprover-community.github.io/archive/\n"}