Ask three mathematicians what it means for a statement to be “true,” and you will not get three versions of the same answer. You will get three different practices, each of which has decided, for its own reasons, to accept a different kind of evidence as sufficient. A human referee reading a 300-page argument line by line and vouching for it with a reputation is doing one thing. A computer kernel checking, symbol by symbol, that every step of a proof follows from a small fixed set of axioms is doing a second, related but distinct thing. A simulation that runs a discretized version of an equation a trillion times and reports a number with error bars is doing a third thing again, and it is not really claiming to have proved anything at all in the first two senses. This article compares those three approaches — human peer review, machine-checked formal proof, and numerical simulation — on the dimensions that actually distinguish them: what kind of certainty each one produces, how far each one scales, how comprehensible its output is to a human being, and what happens when each one is wrong. None of the three is a strictly better version of another. Each buys something the others cannot, and each pays for it somewhere else.
What “peer-reviewed” actually certifies
Traditional mathematical proof is a social technology before it is a formal one. A paper is submitted, an editor selects one or more referees who are experts in the relevant subfield, and those referees read the argument, checking that each step follows and that the overall strategy is sound. If they find no fatal flaw, the paper is published, and the community treats the result as established — not because every reader has personally re-derived it, but because the chain of specific, accountable experts who did check it is willing to stake their judgment on it.
This is an old and largely successful system, but it has a well-documented failure mode: proofs can be long enough, and technical enough, that no human referee can hold the entire argument in mind at once, and subtle errors survive review for years. The clearest illustration is the four-color theorem. Kenneth Appel and Wolfgang Haken’s 1976 proof reduced the problem to checking around 1,900 special map configurations, a case analysis too large for a human to verify by hand — and it relied on a computer program to perform that checking, which is itself a step outside pure human review. The proof was accepted, but mathematicians remained uneasy about a result no person could fully audit, and that unease is exactly what motivated a second kind of proof three decades later, one verified not by a human reading a printout but by a proof-checking kernel: Georges Gonthier’s 2008 formalization of the four-color theorem in the Coq proof assistant, in which the entire argument, including the case analysis, was expressed in a formal language and mechanically checked against Coq’s small trusted kernel [5].
Peer review’s real strength is not infallibility; it is comprehensibility and judgment. A human referee can recognize that a lemma is stated in an unnatural way, that a proof strategy is needlessly convoluted, that a paper’s real contribution lies somewhere its author did not emphasize, or that a “proof” technically checks out but rests on an assumption nobody would actually grant. None of that is a thing a proof-checking kernel does. A kernel checks validity, not insight, elegance, or relevance. Peer review also scales in a way formal proof currently does not: a competent referee can review an argument in an afternoon that would take a formalization team months or years to encode. Its price for that speed is exactly the failure mode above — human attention has a ceiling, and past that ceiling, review quality degrades in ways that are hard to detect from outside.
What a machine-checked proof certifies instead
A formal, machine-checked proof is a different object. In systems such as Lean, Coq, and Isabelle, a mathematical statement and its proof are both written in a formal logical language, and a small, carefully audited piece of software called the kernel mechanically checks that every inference step is a valid application of the system’s underlying logic — no step is taken on trust, and no step is skipped because it seemed obvious. The kernel itself is deliberately kept small (often a few thousand lines of code) precisely so that it, unlike the mathematics it checks, can plausibly be read and audited by a human being. Lean 4, one of the most widely used such systems today, was built specifically to make this checking practical at scale while remaining a general-purpose programming language in its own right [3].
The scale this approach can reach is now well documented. The Feit-Thompson (odd order) theorem — a 254-page 1963 paper establishing that every finite group of odd order is solvable, itself already a landmark of traditional peer review — was fully formalized in Coq over a six-year collaborative effort, producing a machine-checked proof built from newly developed, reusable libraries of formal finite group theory, linear algebra, and Galois theory [4]. The Kepler conjecture, on the densest way to pack equal spheres, received a first proof by Thomas Hales in 1998 that again relied on extensive computer calculation a human referee panel could not fully certify line by line; two decades later, the Flyspeck project completed a full formalization of that proof in the HOL Light and Isabelle systems, published as “A Formal Proof of the Kepler Conjecture” [1]. In both cases the underlying mathematical claim had already been accepted by the community on the strength of traditional review; what formalization added was not a new belief that the theorem was true, but a categorically stronger kind of evidence for it — reduction to a fixed, small, machine-auditable logical core.
Formal verification is not confined to pure mathematics. The seL4 microkernel — an operating-system kernel of roughly 8,700 lines of C and 600 lines of assembly — was formally verified from an abstract mathematical specification down through to its actual C implementation, establishing a mechanically checked guarantee that the code satisfies its specification and contains no crashes, buffer overflows, or a wide class of other defects, for every possible input [2]. This matters for the comparison at hand because it shows the same technology applied to engineering rather than pure mathematics: the guarantee is about a fixed artifact (this kernel, this exact source code), not a general theorem about all kernels of a kind, and the effort required — years of dedicated proof engineering — is the same order of cost that Feit-Thompson and Flyspeck required for pure theorems.
That cost is the honest price of the stronger guarantee. Formalizing an existing, already-accepted theorem routinely takes person-years, requires building extensive supporting libraries from scratch, and produces a proof object that is, by design, largely unreadable as mathematical prose — a human checking the informal argument reads mathematics; a human checking the formalization mostly reads that the formalization typechecks, and separately audits that the formal statement of the theorem actually says what everyone believes it says. That second audit — “does the formal statement match the informal claim?” — is a place where human judgment re-enters even a fully formal proof, and it is not itself machine-checked. A kernel can certify that a proof of a false-to-you statement is internally valid if you have mis-stated the theorem; it cannot tell you that you asked the wrong question.
What a numerical simulation certifies, and what it does not
The third approach abandons proof of an exact statement altogether and instead computes an approximate answer to a question that, in most interesting cases, has no known closed-form exact answer at all. Climate models, structural simulations, fluid dynamics codes, and Monte Carlo integrators are numerical simulations in this sense: they discretize a continuous system, iterate a computation, and report a number together with some estimate of the error introduced by discretization, floating-point rounding, and model uncertainty. The Coupled Model Intercomparison Project (CMIP6), a large multi-institution framework for comparing climate models against one another and against observations, is a mature example of this discipline being run at civilizational scale — dozens of modeling centers running standardized experiments so that the spread across models becomes part of the reported answer, not a hidden embarrassment [8].
Numerical computation has its own internal notion of rigor, and it is worth separating from “approximate, therefore weak.” Interval arithmetic and other verified-numerics techniques can turn an ordinary floating-point computation into one that produces guaranteed bounds — a computed interval that is mathematically certain to contain the true answer, even though the true answer itself is never pinned down exactly. Warwick Tucker’s 2002 resolution of Smale’s 14th problem is the clean example: he did not compute an approximate Lorenz attractor and eyeball that it looked chaotic; he built a rigorous ODE solver using interval arithmetic with directed rounding and proved, with guaranteed error bounds at every step, that the Lorenz equations really do support a strange attractor as Edward Lorenz had conjectured in 1963 [6]. That result sits in an interesting middle zone of this comparison: it is a numerical computation, but one whose output is a certified mathematical proof of a qualitative property (chaos exists here), not merely a plotted trajectory.
Ordinary floating-point simulation, without that verified-numerics discipline, does not offer this guarantee, and the reason is a specific, well-understood mechanism rather than vague “approximation.” Binary floating-point numbers cannot represent most real numbers exactly, and every arithmetic operation on them can introduce a small rounding error; those errors compound differently depending on the order of operations, the conditioning of the underlying problem, and the number of steps in the computation, in ways David Goldberg’s classic 1991 survey of floating-point arithmetic catalogs precisely, down to how catastrophic cancellation, guard digits, and the IEEE 754 standard’s rules for rounding and special values interact [7]. A simulation’s error bars should, when done well, reflect the accumulation of these effects together with the deeper modeling uncertainty of the underlying equations — but unlike a formal proof’s kernel check, there is no single small trusted component whose correctness certifies the whole computation. Trust in a simulation is distributed across code review, cross-validation against other simulations and against observation, sensitivity analysis, and — in the CMIP6 case explicitly — comparing many independent groups’ results against each other, precisely because no one model’s internal consistency is proof of its accuracy.
The complexity dimension separates simulation sharply from the other two approaches. A simulation can, in principle, be run at essentially any scale the available compute allows: more grid points, finer time steps, more Monte Carlo samples, larger ensembles. Cost trades directly and continuously against precision. Neither peer review nor formal proof has that kind of dial. A human referee cannot review “80% as carefully” and get an 80%-as-reliable answer in linear proportion; below some threshold of attention, review quality can fail outright rather than gracefully degrading. A formal proof either typechecks or it does not — there is no partial credit inside the kernel, only degrees of how much of a theory has been formalized so far. This is why an enormous, well-funded push to formalize the entirety of some field of mathematics is a fundamentally different kind of project than “run the simulation twice as long.”
This decomposition is worth writing out because it names what a reported simulation number actually
is: not the true answer
Comparing the three on the dimensions that matter
Laid side by side, the three approaches trade off against each other on at least four axes, and it is worth being explicit that this is analysis, not a ranking — nothing below should be read as “and therefore the best approach is.”
Certainty of what is claimed. A machine-checked formal proof offers the strongest guarantee of logical validity given its stated axioms and its stated formal claim — a claim about a claim, essentially, since the kernel cannot tell you whether the formal statement captures what you meant informally. Traditional peer review offers a weaker, human-bounded guarantee of validity, but a comparatively strong guarantee of relevance and meaning, since a human referee is exactly the entity equipped to notice when a technically valid proof answers the wrong question. Numerical simulation offers no guarantee of exactness at all in the ordinary case, only a quantified estimate of approximate correctness — except in the narrower verified-numerics regime, where it can offer guaranteed bounds on an otherwise-uncomputable exact quantity, as in Tucker’s Lorenz result [6].
Scalability. Simulation scales most freely with compute; formal proof scales only with sustained human proof-engineering effort measured in years, even though systems like Lean 4 have substantially lowered that cost relative to earlier proof assistants [3]; peer review scales worst of the three, bounded by the number of qualified experts willing to spend the necessary time, which is precisely the bottleneck that made the four-color theorem controversial for so long.
Human comprehensibility. Peer-reviewed proof is written to be read; that is its entire point. Machine-checked proof is written to be checked, and is frequently close to unreadable as mathematical prose, which is why formalization projects invest heavily in separately auditing that the formal statement matches an informally understandable one. Numerical simulation output is a number plus error bars — comprehensible as a result but silent on why the underlying system behaves that way, unless paired with separate analytical understanding.
Failure mode when wrong. A flawed peer-reviewed proof fails silently until a reader notices the gap, sometimes years later. A formal proof, once it typechecks, cannot silently contain a step that does not follow — its failure mode moves entirely to the antecedent question of whether the formalized statement was the right one to formalize, or whether an inconsistent axiom was smuggled into the system. A simulation’s failure mode is the quietest and most dangerous of the three: a badly conditioned computation can produce a plausible-looking wrong number with tight-looking, misleadingly confident error bars, which is exactly why multi-model comparison exercises like CMIP6 exist as an institutional check on any single simulation’s self-reported confidence [8].
Where machine-assisted mathematics fits, and where the disagreement is real
A fourth category has emerged that does not sit cleanly inside any of the three above: search systems that use machine learning to find proofs, sometimes in a formal language a proof assistant can then check, sometimes in an informal one a human then reviews. In July 2024, Google DeepMind reported that its AlphaProof and AlphaGeometry 2 systems together reached a score corresponding to silver-medal standard at the 2024 International Mathematical Olympiad, solving four of six competition problems, with AlphaProof formalizing and checking its solutions inside the Lean proof assistant and AlphaGeometry 2 producing a symbolic, human-readable proof of the geometry problem in nineteen seconds — this is DeepMind’s own reported claim, not an independent peer-reviewed replication, and should be read as a vendor claim about a specific, disclosed benchmark rather than a general statement about mathematical capability [10]. The earlier AlphaGeometry system, evaluated on a benchmark of thirty Olympiad geometry problems, solved twenty-five, compared to ten for the prior best automated method and roughly twenty-six for an average human gold medalist on the same set — again DeepMind’s own reported benchmark figures [9].
What makes this genuinely a fourth thing, not merely a faster version of formal proof, is where the uncertainty sits. When AlphaProof’s output is checked by Lean’s kernel, the validity of that specific output is exactly as certain as any other Lean proof — the kernel does not care how a proof was generated, whether by a human over a career or a search process over an afternoon. What is genuinely unresolved, and where mathematicians and machine-learning researchers characterize the disagreement differently, is whether search systems of this kind generalize to problems substantially unlike their training distribution, whether they produce proofs a human would recognize as insightful or only as a valid but unilluminating pile of steps, and how much engineering effort per problem sits behind reported benchmark numbers that are not always disclosed in comparable detail across systems. None of the sources here resolve that disagreement, and treating a single Olympiad benchmark score as evidence about general mathematical capability would be overstating what the result shows.
Prediction: three horizons, and what would falsify each one
Near term (through 2028). Formal proof assistants will keep expanding their standard-library coverage of undergraduate and early graduate mathematics, driven by projects that use machine-checked Lean or Coq libraries as training and evaluation substrate for search systems like AlphaProof. The assumption behind this prediction is that current funding and tooling investment (of the kind reflected in Lean 4’s design goals) continues at roughly its current level [3]. Observable indicator: a steadily growing count of formalized theorems in shared libraries such as Lean’s Mathlib. Disconfirmation condition: if formalization effort stalls or funding is redirected elsewhere for several years running, this prediction fails.
Medium term (2028–2033). Numerical simulation and formal methods will increasingly be used together rather than as competitors — for instance, verified-numerics techniques bounding error in otherwise-ordinary simulations of chaotic or safety-critical systems, following the pattern Tucker established for the Lorenz attractor [6]. Observable indicator: growth in published work combining interval-arithmetic or other certified-numerics methods with large-scale simulation, beyond today’s niche of dynamical-systems theory. Disconfirmation condition: if certified numerics remains confined to small hand-picked problems and does not extend to any production-scale simulation pipeline in this window, the prediction fails.
Long term (beyond 2033), explicitly speculative. It is plausible, though far from established, that some meaningful fraction of new theorems in active research areas will first appear as machine-assisted, formally checked results before a traditional peer-reviewed exposition is written around them — inverting today’s order, where formalization typically follows an already-accepted proof, as it did for Kepler and Feit-Thompson [1] [4]. This assumes continued progress in machine-assisted search of the kind reported for AlphaProof and AlphaGeometry [10] [9], and assumes the mathematical community develops a way to certify a formalized result’s relevance, not just its validity, without a human already knowing the informal theorem first. Disconfirmation condition: if, by the early 2030s, formalization is still overwhelmingly a follow-on activity applied to results already established by traditional means rather than a route to genuinely new discovery, this long-horizon claim should be considered falsified.
The complementarity, stated plainly
None of these three approaches is trying to replace the others, and the strongest evidence for that is how often they appear stacked on top of one another in the cases above rather than substituting for one another. The Kepler conjecture went through an informally reviewed proof reliant on computer case-checking, then a formal verification project that re-derived the same result inside a kernel-checked system [1]. The Lorenz attractor’s chaotic behavior went from a 1963 conjecture based on simulation and physical intuition to a 2002 rigorous proof built from a numerical method disciplined by interval arithmetic [6]. Climate projection relies on numerical simulation for its core computation but requires an institutional-scale multi-model comparison exercise, CMIP6, to do the job that neither a lone referee nor a proof kernel can do for a system this complex [8]. And the newest entrant, machine-assisted search, gets its strongest guarantee only by handing its output to one of the two older systems — a Lean kernel for AlphaProof, human Olympiad judges for AlphaGeometry’s constructions [10]. The honest description of mathematical certainty today is not a contest between these methods but a layered practice that uses each one for the part of the problem it is actually suited to, and that keeps working precisely because none of them pretends to be the other.
