Sources#

Which Artifact Carries the Understanding?#

Question (from Logical vs Intelligible Proof, #oq/now): Where an AI-produced open-problem result exists as both a prose argument and a formalization, which artifact actually carries the understanding, and does the formalization ever change what a mathematician can do with the result?

Short answer. The question assumes that prose and formalization are one proof rendered twice, so that understanding sits in one of them. Every paired case in the corpus breaks that assumption. Once the assumption goes, the question splits into three claims, and the corpus settles two of them:

The formal proof carries certainty about the theorem, not understanding. No source reports anyone learning why a result is true from a large AI-produced Lean artifact. The one expert who read one says it "tells us essentially nothing".
The AI prose is the only candidate carrier, and it is weaker than the question assumes. Where it diverges from the formal proof, it is uncertified. Its documented reception ranges from "not yet digested" to "AI slop". Where understanding is actually reported, it came from a third, human artifact.
The formalization does change what a mathematician can do, in one documented way. It serves as an audit map, showing which prose claims are certified. Every forward-looking use (better refereeing, exposing hidden assumptions) is still a prediction.

What stays open is the comparative claim itself, because the corpus has no instrument for understanding. It also has no case where the formal artifact enabled new mathematics.

Labels used below: documented means a source states it, with its tier. Inference means this wiki's reading across sources.

1. The presupposition fails in every paired case#

Case	Prose	Formalization	How they differ	Status
Navier–Stokes (The Navier–Stokes AI Claim)	OpenAI manuscript	`openai/NavierStokesAndEuler`, AI-produced (GPT-6 Astra, 17 h claimed)	Different argument at two named places. At Lemma 8.6 the Lean proof needs m+5 derivatives where the prose claims m+4, because it sums a different series. At eq. (10.19) it proves a different bound by a different route (Sobolev to $L^2$ in place of an $L^{3/2}$ Riesz bound), valid for all t	documented, `case-study`, pinned commit `f9e8bc5` (Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs)
Erdős 90 / unit distance (FrontierMath Erdős Benchmark)	18 pages, model-generated result	1.2M lines of Lean (`plby/Erdos90`), a separate later effort that the wiki records as human-led	Different scope. "The 18-page paper could simply refer to [a deep] result, whereas the Lean formalization needed to derive it from first principles"	documented, `empirical` (Announcing FrontierMath Erdős). Whether the arguments match lemma by lemma has never been checked
FLT (not an open problem, but the corpus's largest pair)	Darmon–Diamond–Taylor 1995 exposition, human-written	Anthropic's 13.4M lines	Different proof choice. Buzzard: "not the modern proof". The formalization "faithfully follows the early literature" and "adds nothing"	documented, `case-study` (FLT: Anthropic has beaten me to it)
FrontierMath Erdős, five solves	Bloom's informal write-ups, explicitly "placeholders"	Astra's Lean proofs, kernel-checked by Comparator	The prose came after the proof and was written by a human to "highlight the ideas involved". It is a human rendering, not the AI's own argument	documented, `empirical` (FrontierMath Erdős)
OEIS Open, 100 proofs (OEIS Open Benchmark)	GPT-5.6 Sol summaries	accepted Lean proofs	The prose is a model narration of the Lean file, with no human check reported	documented, `empirical` (OEIS Open: How many conjectures can language models turn into theorems?)

Navier–Stokes is the decisive case because it is the only one where someone compared the two artifacts step by step. They are different arguments there. Bastounis, Circelli and Hansen give the mechanism: any compile-until-accepted translation loop "tests whether Y′ proves X′ in Lean. It does not check whether the reasoning in Y has been preserved." When the prose is wrong, "the AI is incentivised to find a different proof" (Statement Drift, translation-drift route). Inference: this is a property of the acceptance criterion, not of one repository. So the prior expectation for any AI-formalized prose proof is divergence somewhere, unless someone checks. The paper's own forecast for OpenAI's Euler formalization ("the likelihood of substantial mistranslations is very high") is a prediction, not a finding.

So "which artifact carries the understanding" has no single referent. In Navier–Stokes, the understanding a reader takes from the prose at Lemma 8.6 is understanding of an m+4 claim that nothing certifies. The kernel certified an m+5 lemma that no one wrote to be read.

2. What the formal artifact carries#

Certainty about the top-level theorem, and nothing further on the documented record. De Toffoli and Duede concede the logical half completely: a Lean formalization "secures certainty" (After Math, practitioner-opinion). That certainty has three documented conditions:

the statement is the intended one (the Clay "C" forcing dispute; Hales's statement-fidelity audit, which he prescribes but does not report anyone doing);
the harness asked the kernel the right question (#print axioms, Kernel-Level Proof Auditing);
the kernel is sound (the 2026 Summer of Soundness Bugs, second-hand via Hales, What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI).

Bastounis et al. concede the theorem's correctness rather than check it.

Understanding from the formal artifact: no positive instance.

FLT. Buzzard, the only named expert in the corpus who spent "many hours looking over the code", says the work "mathematically … tells us essentially nothing" (case-study). He recognises that it is "developing a bunch of relevant mathematical material". Inference: he gets that recognition from understanding he already had of the argument. He did not get the understanding from the code. His own deliverable to the EPSRC is a third artifact: "a dynamic document enabling humans to explore the modern proof", which he expects Anthropic will not build.
Scale argument. "mathematicians will unlikely read millions of lines of Lean code to try to understand" (Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs, argument, not measurement). Three of the five pairs above are 1.2M to 13.4M lines.
Lean's own foundations. Hales applies the same judgment one level down. A consistency route known "only" through "an AI formalization that lacks human exposition" is not satisfying (practitioner-opinion).

3. What the AI prose carries#

It is the only artifact anyone wrote to be read. On the documented record it carries less than the question assumes:

Correctness is uncertified wherever it diverges. This is documented at two Navier–Stokes lemmas. Remark 3.4 says those two "are not the only ones", and a census has not been done.
Reception is negative or deferred. Buckmaster, on his own team's Lean-verified Euler work: the first LLM proof was "the most horrendous I have ever read", and one released paper "can only be described as AI slop" (Quanta, AI Has Solved One of Math's $1 Million Millennium Prize Problems, practitioner-opinion). Bloom on the five FME solves: confident in correctness, "not yet properly 'digested'", with the impact depending "on human experts understanding the solutions" (empirical). OEIS Open's 100 summaries are model narrations that no human checked.
One positive judgment. Bloom calls the AI proof of #548 (Erdős–Sós) "surprisingly short and elegant", and the paper sketches it as a double count over vertex orderings. This is the corpus's only first-hand report that an AI-produced argument was itself intelligible. It is one problem, judged by the curator.

Where understanding is reported, a human re-derivation produced it. Bloom, on #1: "While attempting to understand this proof the second author reinterpreted it in terms of lattices, which he found to be a more natural perspective" (FrontierMath Erdős). In Navier–Stokes, the credit for the understanding went to the human analysts whose cascade strategy both AI teams completed: Fefferman calls Córdoba and Martínez-Zoroa "the heroes of the story". Inference, from two instances plus FLT's planned "dynamic document": the understanding sits in neither of the two artifacts the question names. It sits in a human-made third one, and that is also the artifact Bastounis et al. call the "optimal final product": "both an NL argument and a Lean proof with a semantically faithful translation between the two". No AI-produced open-problem result in the corpus has that third artifact yet. At Navier–Stokes the faithful translation demonstrably does not exist.

4. Does the formalization change what a mathematician can do?#

Yes, in one documented way: it shows which prose claims are certified. Once a formal proof exists, comparing it against the prose shows which prose claims inherit certainty and which do not. In Navier–Stokes that comparison produced the m+4/m+5 finding. A GPT-6 Astra Ultra instance, pointed at the lemma, located the gap in 3 min 24 s (case-study). This is a real change: without the formalization, nothing would separate certified prose claims from uncertified ones. It has two limits. The comparison is "delicate and highly time consuming" when done by hand. And a model locating drift on request is not a model certifying fidelity (Statement Drift §5.1, Meta's textbook claim caught by humans).

In process, not product: documented, but the wrong unit. DeepMind's collaborators found failed formal sketches clarifying, because the sketches pointed experts at unresolved subgoals (AI-Driven Formal Proof Search). That is the partnership teaching the mathematician in the loop. It is not the finished artifact teaching the field (Logical vs Intelligible Proof, "strongest counter-evidence").

Prospective, all prediction. Buzzard expects autoformalization to "make the review process … far less painful", to "ruthlessly flag arguments which are incomplete", and to expose what is "known to the experts" in the Langlands literature. Erdős 90's 1.2M lines derived a deep result from first principles. Inference: that adds formal infrastructure that future formalizations can reuse. The corpus does not say whether it reached mathlib, and infrastructure is not understanding.

No documented case of a formal artifact enabling a mathematician to prove something new, generalise the result, or transfer its technique. Those are the "use to make further progress" clauses of De Toffoli and Duede's intelligible notion.

What remains open#

The comparative claim cannot be measured. "Carries understanding" has no instrument anywhere in the corpus. This is the sibling #oq/source question on Logical vs Intelligible Proof. §2 and §3 rest on testimony and absence of reports, not on a test.
The non-dissolved form has no instance. The corpus has no AI-produced open-problem result whose prose and formal proof were checked lemma by lemma and found to be the same argument. The Erdős 90 pair is the cheapest candidate to check.
The product-teaches-the-field case is missing. No source shows a formal artifact (as opposed to a human re-derivation or a collaboration) changing what mathematicians can do beyond auditing. The #oq/wait trigger on Logical vs Intelligible Proof covers the related event: the first AI resolution described as teaching mathematicians why.
Whether the third-artifact pattern generalises. It rests on Bloom's #1, the Navier–Stokes credit, and Buzzard's planned document. That is two documented instances and one intention.

Sources drawn on#

The Navier–Stokes AI Claim, Statement Drift, Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs: the divergence at Lemma 8.6 and eq. (10.19), the acceptance-criterion mechanism, the 3 min 24 s model check, and the "optimal final product" and "millions of lines" passages (§5.2).
FrontierMath Erdős Benchmark, Announcing FrontierMath Erdős, FrontierMath Erdős: the Erdős 90 scope difference, the "placeholders" and "not yet digested" passages, Bloom's lattice reinterpretation of #1, and "short and elegant" for #548.
Kernel-Level Proof Auditing, FLT: Anthropic has beaten me to it: Buzzard on FLT ("tells us essentially nothing", not the modern proof, the dynamic-document deliverable, his review predictions).
Logical vs Intelligible Proof, After Math: the logical/intelligible distinction and the concession that formalization "secures certainty".
AI Has Solved One of Math's $1 Million Millennium Prize Problems: Buckmaster's verdicts and Fefferman's credit.
What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI: the soundness conditions and the human-exposition judgment on Con-Leche.
OEIS Open Benchmark, OEIS Open: How many conjectures can language models turn into theorems?: the model-narrated summaries.
AI-Driven Formal Proof Search, Advancing Mathematics Research with AI-Driven Formal Proof Search: process-side understanding from failed sketches.
Latent Capability Overhang: the identification of the unit-distance disproof as Erdős 90.

Which Artifact Carries the Understanding? Prose and Formal Proof as Two Objects