HN Debrief

Are We Stuck with Lean?

  • Programming
  • Developer Tools
  • AI
  • Mathematics
  • Open Source

The MathOverflow post argued that Lean's momentum may be narrowing the practical space for formalized mathematics, especially for people who want different foundations than Lean's dependent type theory or who prefer systems like Metamath. The key background point is that proof assistants are not interchangeable syntax skins. Each one bakes in different tradeoffs around foundations, kernel size, automation, readability, and library depth. That matters because a formal proof is only useful if it can be expressed in the system you chose and can reuse enough prior work to keep the cost sane.

If you are choosing a proof system now, optimize for existing libraries, automation, and your collaborators rather than for abstract foundations debates. Also treat cross-system portability and machine-generated proofs as open engineering problems, not solved facts.

Discussion mood

Mostly pragmatic and mildly skeptical. People were not panicked about Lean dominance, but they did see strong ecosystem lock-in. The thread was enthusiastic about alternatives like Metamath and Isabelle for specific reasons, while also skeptical of grand claims that LLMs have already solved portability, formalization speed, or proof reliability.

Key insights

  1. 01

    Metamath trades ergonomics for auditability

    Metamath earns its niche by making the trusted core tiny and the proof object brutally explicit. That buys very fast verification and easier independent reimplementation, which is exactly what you want if your priority is minimizing hidden machinery. The cost is equally clear. Proofs are low level, automation is sparse, and the burden of encoding logical infrastructure moves out of the kernel and into the database, so you gain transparency rather than escaping trust altogether.

    Use Metamath when kernel simplicity and independent verification matter more than authoring speed. Do not expect it to be a drop-in replacement for a modern interactive prover with tactics and high-level automation.

      Attribution:
    • dwheeler #1
    • leonidasrup #1
  2. 02

    Library network effects dominate foundation purity

    The decisive advantage is not that Lean settled some deep foundations question. It is that a big installed base and a thick standard library let researchers formalize one local result instead of rebuilding prerequisites. That makes prover choice socially coupled in a way ordinary personal tools are not. Once a community commits, switching costs explode because proofs are not portable text files.

    Pick the ecosystem that already contains the definitions and lemmas your field needs. If you are building a team or program around formalization, budget for lock-in from day one.

      Attribution:
    • pverheggen #1
    • seanhunter #1
    • andrewflnr #1
    • joe_the_user #1
  3. 03

    Isabelle already covers part of the AI promise

    Isabelle's Sledgehammer was presented as the strongest reminder that pre-LLM automation is already useful in research workflows. It can often find proofs or counterexamples quickly from theorem statements plus sensible intermediate lemmas, which gets surprisingly close to the desired "formalize as you go" experience for some fields. The catch is expressiveness. Isabelle's higher-order logic gives up some of the dependent-type power that Lean users want, and that tradeoff is part of why the automation works as well as it does.

    If your work benefits more from automated proof search than from the most expressive type theory, benchmark Isabelle before defaulting to Lean-plus-LLM. The right tool may be the one with stronger automation today, not the one with louder AI momentum.

      Attribution:
    • wizzwizz4 #1
  4. 04

    Lean wins partly as a programming language

    One commenter who switched from Haskell to Lean argued that Lean's edge is not just theorem proving. It is that the host language is good enough to make tactic code, proof engineering, and ordinary programming feel unified. That matters because large formalization projects are software projects. A prover with elegant foundations but weak day-to-day programming ergonomics will lose users to one that lets them extend the system comfortably.

    Evaluate proof assistants like language platforms, not just logic kernels. Metaprogramming, tactic authoring, and general developer experience can matter as much as the underlying foundation.

      Attribution:
    • Syzygies #1
  5. 05

    LLMs help with syntax more than mathematical taste

    The strongest AI-related point was not whether models can produce checked code. They can. The problem is that formal mathematics becomes valuable when definitions, abstractions, and proof structure are elegant enough to reuse and understand. Several commenters said models are better at grinding out local arguments than at choosing the right general formulation, which is exactly the part that turns one-off formalization into a durable library.

    Treat LLMs as accelerators for local proof completion and boilerplate. Keep humans in charge of definitions, abstraction boundaries, and anything meant to live in a shared library.

      Attribution:
    • quasisphere #1 #2
    • wizzwizz4 #1
  6. 06

    Kernel exploits are bugs, not the main trust model

    The security discussion sharpened an important distinction. A proof assistant rejecting honest mistakes is not the same thing as a proof assistant safely validating malicious artifacts crafted to exploit implementation bugs. Lean commenters pointed to published guidance that this adversarial case is known and treated as a software bug class, but not the central operating assumption for ordinary mathematical use. That makes sensational examples less damning for day-to-day research than they first appear.

    If you use formal proofs in adversarial settings like software supply chains, add independent validation and a stricter review pipeline. For ordinary math, do not confuse a kernel bug with a collapse of the whole proof-assistant model.

      Attribution:
    • andrewla #1
    • seanhunter #1

Against the grain

  1. 01

    LLM speed may overwhelm elegance concerns

    The bullish case was that line-count explosions from systems like Sol are not a sideshow but the beginning of mass autoformalization. On that view, the bottleneck is no longer whether humans can elegantly curate every proof. It is whether machines can ingest the historical literature fast enough to make it searchable, checkable, and available for later cleanup. Critics called lines of code a junk metric, but the contrarian point is that crude volume may still change the economics first.

    Watch for workflows where ugly machine-generated formalizations are useful before they are beautiful. If retrieval and checking matter more than pedagogy, throughput can beat elegance for a while.

      Attribution:
    • pfdietz #1 #2
    • voxl #1
  2. 02

    Translation between provers may become cheap

    A minority view held that today's lock-in may not last because models can sit above prover languages and treat them as compilation targets. If that works, the human-facing layer becomes closer to ordinary math prose, while the specific checker underneath matters less. That would weaken current ecosystem moats and make cross-checking across multiple provers more realistic than it looks today.

    Do not assume current proof-language silos are permanent. If interoperability is strategically important, invest in clean theorem and definition representations now so they are easier to translate later.

      Attribution:
    • hawtads #1
    • or_am_i #1
    • quasisphere #1

In plain english

autoformalization ↩
The process of turning informal mathematics, such as textbook prose or papers, into machine-checkable formal proofs.
dependent type theory ↩
A family of type systems where types can depend on values, allowing programs and proofs to be expressed in the same formal language.
Haskell ↩
A functional programming language with a powerful type system, but not a standard interactive theorem prover.
kernel ↩
The small trusted part of a proof assistant that checks whether proofs are valid.
Lean ↩
A theorem prover and programming language based on dependent type theory, widely used for formalized mathematics.
LLM ↩
Large language model, a machine learning system trained to generate and understand text.
Metamath ↩
A proof language and verifier designed to keep the trusted core extremely small and make every proof step explicit.
Sledgehammer ↩
An Isabelle tool that uses automated reasoning systems to search for proofs or counterexamples.
tactics ↩
Proof-building procedures that automate or structure steps in an interactive theorem prover.

Reference links

Metamath references

Proof assistant automation and trust

LLM and formalization claims

Other tools and projects

  • F*
    Raised as a possible better fit for non-mathematics verification projects.
  • Low* introduction
    Provided as an example of F* for low-level verified software.
  • Emacs Evil mode
    Shared jokingly in the editor analogy about tool rivalry.