What a proof assistant promises

A proof assistant checks an argument expressed in a precisely defined language. The author supplies definitions, assumptions and proof steps; the machine checks the permitted inferences. That makes it possible to revisit an enormous argument without relying entirely on a person’s memory or another person’s assurance. Understanding what the argument means remains a mathematical task.

A small example of the promise

Consider the statement “every number has a square root.” It changes meaning when “number” means a nonnegative real number, an arbitrary real number, or a complex number. A checker needs the domain stated precisely. It can then check a proof of that statement, but a correct proof about complex numbers does not establish the claim about all real numbers.

There is a second distinction. Suppose a written proof gives a wrong reason for a true statement. A system might discover a different, correct proof. The theorem is then supported, while the original reasoning still needs correction. These distinctions matter especially when AI translates mathematics into a proof language.

Six systems, six emphases

Lean is a proof assistant and functional programming language begun by Leonardo de Moura in 2013. Its community library, mathlib, joins algebra, analysis and other mathematics in a shared development. Contributors collaborate through reviews, discussion and project blueprints that connect prose to formal dependencies. Its mathematical visibility rests on substantial projects, including the Liquid Tensor Experiment and sphere eversion. The latter proves that a sphere can be turned inside out while remaining smooth, allowing the surface to pass through itself.¹²³

Rocq, called Coq in older work, began at Inria in 1984. It connects mathematical proofs with precisely typed programs. Its Mathematical Components community developed reusable algebra while formalizing the four-color theorem and the odd-order theorem about finite groups. Rocq also supports compiler verification, including CompCert. That application checks a relationship between program behaviors, which is a different achievement from proving a mathematical classification theorem.⁴⁵⁶

Isabelle grew from Lawrence Paulson’s work in the 1980s. It supports several logics; most mathematical users work in Isabelle/HOL. Its Isar language lets authors organize assumptions and intermediate claims into readable proof text, with automated methods checking individual steps. The Archive of Formal Proofs, or AFP, publishes reviewed developments. They include an analytic proof of the prime-number theorem, which describes the large-scale distribution of primes.⁷⁸

Mizar starts from Andrzej Trybulec’s 1973 proposal for a mathematical language. Its structured proofs deliberately resemble mathematical writing, with a controlled vocabulary and explicit references. Its Mathematical Library, MML, grew through articles and library review, and the journal Formalized Mathematics continues to publish this work. Its set-theoretic foundation and writing style offer a useful contrast to the programming-oriented surfaces of Lean and Rocq.⁹¹⁰

Agda comes from the constructive type-theory tradition at Chalmers; its current lineage follows a redesign documented in 2007. Authors commonly build a proof as a typed function. “Constructive” means that existence claims often carry a way to produce the object, rather than only an argument that it cannot fail to exist. Cubical Agda adds machinery suited to mathematics about paths and spaces. Its community has formalized concrete calculations of cohomology rings, algebraic descriptions of features of spaces.¹¹¹²

Arend is a separate JetBrains Research project developed from 2015. Its foundations also support mathematics about paths and equivalent structures. It has a mathematical library and published research artifacts, including a constructive theory of complete spaces. Its August 2026 release documents continued work in algebraic geometry and analysis. Those are signs of a specialized research community; they do not establish a large user population.¹³¹⁴¹⁵

Why the older systems still matter

The history runs through different ideas about expressing mathematics, rather than a single sequence of replacements. Mizar emphasizes mathematical articles; Rocq and Agda connect proofs with programs; Isabelle separates a general framework from particular logics. Lean’s shared library and recent collaborative projects supply another route. Arend and Cubical Agda explore foundations in which paths and equivalences play a direct role.

HOL Light and HOL4 are also established members of the landscape. HOL Light, together with Isabelle, supported Flyspeck’s formal proof of the Kepler sphere-packing conjecture, completed in 2014. Metamath offers another contrast: a minimal proof language with databases that state their own axioms, and multiple independent programs that check its principal databases.¹⁶¹⁷

What to conclude from the news

Lean’s recent results deserve attention, but a headline can combine several different accomplishments: encoding a known proof, finding a new argument, checking a particular statement, and producing an explanation people can assess. Each deserves its own evidence. OpenAI’s recent Navier–Stokes claim concerns smooth forcing that makes an initially stationary fluid develop unbounded velocity in finite time. An October critique identifies differences between intermediate written claims and their formal counterparts, while leaving the written proof’s correctness unjudged.¹⁸ The dispute illustrates why checking a theorem and validating its accompanying argument are separate tasks.¹⁹

No language automatically knows which informal theorem its author intended. A familiar-looking statement can conceal a changed domain, a missing assumption or a differently defined object. Readable proofs, independent checking and expert review address different parts of that problem. The choice among systems therefore depends on the mathematics already available, the community able to help, and the kind of explanation one wants to preserve.

Problem space

• Understand the mechanism: report 2 explains how proof search differs from checking.
• Inspect a claim: identify the precise statement and its assumptions before interpreting “verified.”
• Terminus: this orientation supplies the vocabulary needed to read the comparison without a programming background.