In situ Formalization
Faithful formal proofs for AI-generated mathematics
This post was written in collaboration with Jonas Bayer. Thank you to Malte Hassler, Quentin Vermande and Annie Yao for feedback. It is based on joint work with many others, and it has been an honor to work with them. Special thanks to the ENS Mathematics Department (DMA) for funding our formalization project back in 2021, when this topic still belonged to an esoteric niche of mathematics.
Recent advances in artificial intelligence (AI) have made large language models (LLMs) a source of candidate proofs for open mathematical problems, at a scale that human refereeing cannot match. OpenAI recently released over 700 AI-generated manuscripts on open problems, but three were withdrawn soon after their release, and the status of many claims is unverified. Formal verification in an interactive theorem prover (ITP) such as Isabelle, Rocq or Lean is widely seen as the remedy. An ITP, however, certifies only that a proof establishes its formal statement. Whether that statement means what the natural-language text claims lies outside the checker, and checking it remains a human task that does not scale with AI output.
We call a formal proof semantically aligned with an informal one if its formal statements, read with the definitions they rely on, say what the corresponding informal statements claim. For the main theorem, alignment decides whether the formal proof establishes the claimed result; for intermediate statements, it decides whether the formal proof can be trusted as a companion of the informal one.
Figure 1. Checking proofs versus checking meaning. An interactive theorem prover (ITP) verifies that a formal proof establishes its formal statement.
Semantic alignment currently fails in practice. OpenAI’s announced proof of blow-up for the Navier–Stokes equations was released with a Lean formalization, but Bastounis et al. find estimates in the paper that differ from what the Lean code proves, and Avigad et al. report that many informal and formal texts in OpenAI’s larger release diverge in subtle or significant ways.
What, then, keeps formal and informal statements aligned? Part of the answer lies in shared, human-curated formal libraries, which increasingly attract research mathematicians. A formal statement can be no more faithful than the definitions it builds on, so Avigad et al. encourage projects to use existing vetted statements of problems wherever possible. The other part, and the focus of this post, lies in how a formalization is produced.
We present what we call in situ formalization: the informal and the formal proof are developed in parallel within the same research group, each shaping the other, so the two stay in sync. The name reflects that the proof is formalized in its natural environment, a mathematics department, under the direction of its own authors. The usual approach is to formalize a finished paper or manuscript afterwards—one might say in vitro. Bastounis et al. argue that faithful autoformalization is unattainable in principle, but their argument assumes a fixed text to be translated, whereas in situ both texts change together.
Our case study is a quantitative undecidability result for Hilbert’s Tenth Problem over the integers, whose formal proof was written entirely by humans between 2021 and 2025. Because the formal statement was written alongside the theorem itself, semantic alignment was never a separate translation step. The formalization in fact corrected our main result, the degree bound of the universal Diophantine equation we construct: early announcements, including our first preprint, claimed a result (\(1.63 \cdot 10^{63}\)) that was 3% stronger than the proof supported; the verified bound is \(1.68105 \cdot 10^{63}\).
Figure 2. In vitro versus in situ formalization. In vitro, the informal proof is fixed before it is formalized, so failures are repaired only on the formal side and misalignments surface after publication. In situ, both proofs are developed together toward the authors’ intended result, so a failure can correct and align both proofs before publication.
Case study: mathematical results
Hilbert’s Tenth Problem asks for an algorithm to decide, for every Diophantine equation (polynomial equation with integer coefficients), whether it has a solution in the integers. Davis, Putnam, Robinson and Matiyasevich showed that no such algorithm exists: every recursively enumerable set is Diophantine, a result now known as the DPRM theorem. Hence, for every Turing machine there is a Diophantine equation that has a solution if and only if the machine halts, so an algorithm for Hilbert’s Tenth Problem would decide the halting problem. In particular, there are universal Diophantine equations that encode all others, for which Matiyasevich and Jones gave an explicit construction. Since Diophantine equations can also encode open problems such as Goldbach’s conjecture and the Riemann hypothesis, it matters how simple such equations can be.
We measure this by the number of integer unknowns \(\nu\) and the degree \(\delta\). Equations in a single unknown are decidable, and so are equations of degree at most two by a theorem of Siegel. Our result bounds both complexity measures at once.
Theorem. There is no algorithm that can decide all Diophantine equations with at most eleven unknowns and of degree at most \(1.68105 \cdot 10^{63}\).
Matiyasevich and Jones had proved analogous bounds for equations with unknowns in the natural numbers, for instance undecidability with nine unknowns in \(\mathbb{N}\) and degree at most \(1.64 \cdot 10^{45}\), or with 58 unknowns and degree four. Translating these to the integers (which matches Hilbert’s original question) naively requires three integer unknowns for each natural one, hence at least 27 unknowns in \(\mathbb{Z}\). Building on a construction of Sun, we instead turn any such equation \(P\) into an equation \(Q\) with eleven integer unknowns1 that has a solution if and only if \(P\) does, at the price of a much larger degree.
Call a pair \((\nu, \delta)_{\mathbb{N}}\), resp. \((\nu, \delta)_{\mathbb{Z}}\), universal if every Diophantine set can be represented by a parametric equation with at most \(\nu\) unknowns in \(\mathbb{N}\), resp. in \(\mathbb{Z}\), and of degree at most \(\delta\). The precise statement we formally proved is the following.
Formalized Theorem. Let \((\nu, \delta)_{\mathbb{N}}\) be universal. Then,
\[(11, \eta(\nu, \delta))_{\mathbb{Z}}\]is universal, where \(\eta : \mathbb{N}^2 \rightarrow \mathbb{N}\) is given by
\[\eta(\nu, \delta) = 15\,616 + 233\,856 \, \delta + 233\,952\, \delta\, (2 \delta + 1)^{\nu + 1} + 467\,712 \, \delta^2\, (2\delta + 1)^{\nu + 1}.\]
Applied to the universal pair \((58, 4)_{\mathbb{N}}\) of Matiyasevich and Jones, it yields the Theorem above. The full proof appears in our article, and its formalization in the Archive of Formal Proofs and our ITP 2025 paper.
Since then, Sun has reduced the best-known number of integer unknowns to ten, and AI-generated proofs have appeared in this very area. For example, over the Gaussian integers \(\mathbb{Z}[i]\), Ding and Li improved a bound of Matiyasevich and Sun from 20 to 18 unknowns using AI, and OpenAI claims to have resolved Hilbert’s Tenth Problem over \(\mathbb{Q}\).
Impact of the in situ formalization
Our in situ formalization was completed in mid-2025, before LLM-based autoformalization contributed at research level. Instead, a team of 13 contributors, primarily undergraduate students at the time, contributed significantly to the formalization. It comprises about 20,800 lines of Isabelle in 47 theory files, with roughly 670 lemmas and theorems, compared to a 56-page article. About 4,000 of these lines are general-purpose infrastructure for multivariate polynomials, including the degree automation described below. The remainder has a de Bruijn factor of about 4.4: measured by compressed size, it is 4.4 times as large as the article’s proof sections, which is comparable to values measured for other formalizations. Our formalization mirrors the article lemma by lemma, and the article links every result to its formal counterpart in the Archive of Formal Proofs, so that the two can be compared directly.
We summarize three lessons about how the back-and-forth kept the two versions aligned. The effect of our method on the proof is also documented in detailed remarks throughout the full article, and a final section discusses it in retrospect.
First, translating our informal draft into Isabelle repeatedly forced it to become exact. One lemma turned out to be unprovable as stated because hypotheses were missing; others lacked edge cases that were later needed, such as a lemma on Lucas sequences proved for \(A > 2\) but used for \(A = 2\). Our draft had also asserted a lower bound without justification, and its proof took about 500 lines of Isabelle and half a page in the final article. Formalization also exposed unnecessary hypotheses, because deleting one in the formal proof immediately flags whether and where the argument relies on it. This revealed a superfluous assumption in our coding theorem, needed only in a more general version due to Sun.
Second, the translation sometimes ran the other way, from the formal to the informal proof. A key lemma had been missing from our draft for several years, and our first pen-and-paper proof of it was wrong. Meanwhile, the team formalizing a result that depended on it had found a correct proof of the lemma on their own. When the error surfaced late in writing, we translated the formal proof—close to 2,000 lines, with many auxiliary results missing from the manuscript—back into four new pages of the article. Isabelle’s structured proof language let even coauthors who had never formalized read it and check it against the text, and the typeset proof of Lemma 3.10 in our article now mirrors the hierarchical structure of the formal proof. The improved exposition is a benefit of in situ formalization beyond the semantically aligned certificate of correctness.
Third, all this costs effort. Informal mathematics tolerates ambiguity that a proof assistant does not: each polynomial of our construction had to be defined both as a function and as a formal polynomial, and the two definitions had to be related by proof. We also formalized every cited result that the Formalized Theorem relies on rather than assuming it, so that no cited theorem enters as an unchecked axiom whose statement might not match its source. Distributing the work required an early top-down skeleton of the entire proof. Keeping manuscript and formalization aligned then had a price, because every change to a statement, even relabeling a variable, had to be coordinated with the formal development. Some of these costs, however, could be reduced by automation.
Automating formal proofs
Besides the dual representations described above, our main computation, the final degree bound, relies on a simple algorithm that an article would not mention, namely bounding the degree of a polynomial by taking maxima over summands and sums over factors. Proving each such step correct by hand would not have scaled to the dozens of polynomials in our construction.
We therefore extended Isabelle with two commands: poly_extract turns an ordinary function into a formal polynomial and proves that the two agree, and poly_degree computes an upper bound on the total degree of such a polynomial and proves the bound correct. For instance, the polynomial \(Q\) with eleven integer unknowns from above is defined in Isabelle as a function Q_tilde \(: \mathbb{Z} \times \mathbb{Z}^{11} \to \mathbb{Z}\). The two lines
poly_extract Q_tilde
poly_degree Q_tilde_polyfirst generate the formal polynomial Q_tilde_poly \(: \mathbb{Z}[a, z_1, \ldots, z_{11}]\) and prove it agrees with Q_tilde upon evaluation, and then compute and prove an upper bound on its total degree. Simplifying the resulting bound yields the function \(\eta\) from above and thereby formally proves the corrected degree bound, a 64-digit number. The incorrect bound in our first preprint came from a mistake in an earlier version of \(\eta\) that careful use of computer algebra had failed to catch. This makes semantic alignment partly mechanical. The commands reduce what has to be aligned to one definition per polynomial, written as a function that reads like its formula in our manuscript, with the remaining formal objects derived and proved automatically.
On semantic alignment for AI-generated mathematics
Our work was done entirely by humans, but let’s explore how this verification method translates to AI-generated mathematics.
Status quo. Most large-scale formalizations to date are in vitro: they verify proofs that have already been published, such as the recent formalization of sphere packing in dimension 8 by Hariharan et al. Closer to our approach, the Liquid Tensor Experiment formalized a recent, not yet refereed theorem of Clausen and Scholze, with Scholze directly involved. Completed by Commelin et al. in 2022, it showed that ITPs can aid progress in mathematics by building on formalized libraries of knowledge.
Such projects typically keep formal and informal text aligned through a blueprint, a natural-language document that breaks the informal proof into small definitions and lemmas, links each to its formal counterpart, and displays their dependency graph. Tao’s formalization of the polynomial Freiman–Ruzsa conjecture and the formalization of Fermat’s Last Theorem led by Buzzard are organized this way. A blueprint shares a key feature of in situ formalization: informal and formal statements are written side by side and revised together as the formalization proceeds.2 It differs in that it is usually written for a proof that already exists, rather than alongside the original research.
In two recent open online collaborations, formal verification became part of the research itself. The Busy Beaver collaboration ultimately determined BB(5) = 47,176,870 using the Rocq theorem prover. As in our work, the theorem prover removed the need to review each contributed proof by hand and was crucial for computing and verifying a large natural number. The Equational Theories Project, launched by Tao, worked in Lean from the start to settle all 22,028,942 implications between 4,694 equational laws on magmas. Both problems decompose into a vast number of small, comparable cases whose formal statements are generated mechanically, so their alignment with the informal claims is comparatively easy to check. Most research mathematics, by contrast, admits no such decomposition, and for AI-generated formal proofs in particular, correspondence with the informal proof is a central difficulty, as the examples below illustrate.
AI models now also produce research-level formalizations, in part or in full, and Table 1 of Ilin lists examples from early 2026. The two OpenAI releases from the last two months are among the most prominent, and both were formalized in vitro. The Lean proof of Navier–Stokes blow-up was released together with the paper, but it was produced only after the natural-language proof had been found. Of the over 700 manuscripts, only about 42% have Lean formalizations of their main results, and further formalizations are added as they are obtained, after publication of the informal text. In both cases the formal proofs are machine-checked, yet misalignments were found only later, by outside readers.
Faithful formalization in practice. Semantically faithful (auto-)formalization has been claimed to be unattainable in principle. Bastounis et al. argue that a faithful autoformalizer would first have to decide whether a presupposed object, such as “the least \(n\) with a given property,” exists. In Lean, for instance, partial operations are often made total, so the least element of a possibly empty set of natural numbers defaults to zero. A formalization can therefore compile although a presupposed object does not exist, and this can go unnoticed whenever the proof does not depend on it. They show this decision problem to be harder than the halting problem, using, as it happens, a universal Diophantine equation of exactly the kind we study.
Their argument concerns translating a given text as it stands. But if we formalize in situ, the text is not fixed, and neither human nor AI formalizers need to make such a decision. Instead, a presupposition that cannot be resolved is stated as an explicit hypothesis, in the formal and the informal statement alike. The autoformalizer then no longer needs to resolve it during translation, and both statements change visibly. Whether it holds becomes a new question, and the formalization exposes it to the reader.
Toward in situ autoformalization. In situ formalization changes how semantic alignment is checked (Figure 2). When a finished text is formalized in vitro, the informal side is immutable and the formal proof tries to mirror it. For an AI system, any formalization that compiles then naively counts as success, even one that departs from the informal argument. When both are developed together, a failed formalization can instead prompt edits to the informal text. In our project, some lemmas turned out to be unprovable as initially stated, and a wrong pen-and-paper proof was replaced by a re-translation from the formalization. Semantic alignment is thus checked continuously, in both directions and before publication. In blueprint-based projects, the blueprint plays this role; in ours, the manuscript itself did, and it links every result to its formalization. Beyond alignment, the same process can also serve human understanding. For example, the in situ formalization improved the exposition of our natural-language article, something formal verification alone does not do.
For AI-generated mathematics, this suggests incorporating formalization into the research rather than checking arguments after the fact, as in the releases discussed above. Every intermediate result should be linked to its formal counterpart, not only the main theorem. Without such links, readers must reconstruct the correspondence themselves. For the Navier–Stokes paper, Bastounis et al. compare its estimates with the Lean theorems that “appear to bear the closest resemblance” and find that several of these estimates claim more than the Lean code proves. Where possible, semantic alignment should further be made mechanical, as in the Equational Theories Project, which generated the formal definition of each law automatically, or as with our commands, which partially automate the formal definitions of polynomials and their properties.
The same loop can fail in reverse. A system that writes both texts could resolve a mismatch by weakening the informal claim to whatever it proved formally. For a claim that was wrong, as some of our lemmas and even our main degree bound were, this is a correction, but when it replaces the intended result, it is a failure. To prevent this for well-studied problems, repositories such as lean-eval and Formal Conjectures contain trusted statements that can be used as a fixed target. For example, OpenAI’s Navier–Stokes proof can be checked against a fixed Formal Conjectures statement. However, new mathematical research rarely has a trusted formal statement in advance. The human authors then have to decide which changes may pass between the two texts, and in which direction.
Formalization at research scale has so far been costly. Our project took four years with 13 people contributing to the formalization. For comparison, the Liquid Tensor Experiment took a year and a half with 18 contributors, the Busy Beaver collaboration about two years, and the Equational Theories Project seven months with over fifty contributors. Our project was feasible because the ITP checks every contribution, which turned the subgoals of our proof into well-defined tasks, so that new contributors could pick up where others had left off. The same guarantees let AI agents take over this work. If they claim to solve open problems en masse, it is reasonable to expect them to develop a formal proof alongside the informal one.
Conclusion
We have argued that the semantic alignment of AI-generated formal proofs depends on how a formalization is produced. An interactive theorem prover only checks proofs, not meaning, so whether a formal statement says what its informal counterpart claims remains a human judgment. This distinction matters because AI-generated mathematics cannot be refereed by humans at scale, and formal verification has to carry much of the load. But a formal proof produced after the fact may compile even if its statements depart from the informal ones. For many recent AI-generated results, alignment was checked only after publication, and readers have since found several misalignments.
AI agents should therefore formalize in situ, while the proof is being developed and both texts can still change. When the informal and the formal proof are written together, with the same authors in charge of both, mismatches surface as lemmas that cannot be proved as stated, and they can be resolved before publication. Faithful formalization of AI-generated mathematics is thus within reach in practice, whatever its difficulty in principle.
Our formalization of a quantitative undecidability result for Hilbert’s Tenth Problem over the integers, carried out entirely by humans, shows that this method can work at research scale. The formal proof corrected our main result, and the article now links every result to its formal counterpart in Isabelle’s Archive of Formal Proofs. Formalization also made our informal proof simpler in places and clearer in others. We expect the same when AI agents formalize in situ, and clearer proofs in turn make misalignment easier to detect.
We derive the following recommendations for producing AI-generated mathematics.
- Formalize before the informal proof is finished, so that it can still be corrected where the formalization fails.
- Link every result to its formal counterpart (not only the main theorem) and record whether and where the formalization diverges.
- Keep the authors in charge of meaning. They decide what the main result must say, using a vetted formal statement where one exists, and they resolve mismatches as they arise, even when an AI system writes both texts.
Formalization at research scale has been slow and costly, which is why proofs are usually formalized only once they are finished, if at all. In our project, humans did most of the formalization, but AI agents are increasingly taking their place. Once they bear the cost, nothing forces the formal proof to wait for the informal one, and in situ formalization can deliver formal statements that mean what they claim and informal proofs that are easier to understand.
In 2012, and again verbatim in 2024, Matiyasevich predicted:
In 25 years mathematical journals (if they are destined to survive so long) won’t take into consideration any paper unless it is accompanied by proofs which can be verified by a computer.
Our result already meets this standard, in its intended meaning, by a computer-verified proof that is semantically aligned with the article. As AI-generated mathematics creates the need and AI-assisted in situ formalization the means, this prediction may well come true ahead of schedule.
This polynomial is denoted \(\tilde Q\) in our article and formalization. ↩
Tools such as LeanArchitect now generate much of a blueprint from annotations in the Lean code itself and infer its dependency graph automatically. ↩
Leave a Comment