Logical vs Intelligible Proof

Sources#

Summary#

Silvia De Toffoli (IUSS Pavia) and Eamon Duede (Princeton/Purdue) argue, in a guest post on Terence Tao's blog four days after [[navier-stokes-ai-claim|OpenAI's Navier–Stokes announcement]] (After Math, 2026-09-12, ~2,000 words, practitioner-opinion), that there are two notions of proof and the corpus's whole verification apparatus only addresses one of them:

The logical notion. "Modern logic characterizes proof in terms of deductive validity such that a proof can be checked by a mechanical procedure that does not itself require understanding of the mathematical argument." They state plainly that "a Lean formalization meets these standards exactly" and that a Lean formalization of Navier–Stokes is therefore "a genuine and important contribution: by meeting the demands of the logical notion of proof, it secures certainty."
The intelligible notion. Mathematicians also "want to know what makes a proposition true. This kind of knowledge trades in mathematical ideas that they can grasp, communicate to other experts, connect with existing knowledge, and use to make further progress."

Their claim is conjunctive: "Genuine proofs are at the same time logical and intelligible proofs," and "falling short of either the logical or intelligible notion creates roadblocks where genuine proofs clear the way for mathematical progress." On that reading OpenAI produced "an answer, not a solution" — the analogy they use is Deep Thought's 42 — and the Clay Mathematics Institute's own Navier–Stokes page is their supporting witness: proof matters "Because a proof gives not only certitude, but also understanding."

This is an argument, not a measurement. It is on this wiki because it names a property that no verification mechanism in the corpus checks, and because it is the only source in the 2026-09 formal-math batch with no lab affiliation and no result to defend.

Why the two notions used to be the same thing, and why they aren't now#

The historical claim is the load-bearing one. De Toffoli and Duede argue the two notions "have tended to run together" for a contingent reason: "no mathematician could produce an enormously complicated logical proof without first grasping some of the key shareable ideas that made the theorem true." The logical notion was therefore used "primarily… to verify the correctness of intelligible proofs" (they cite Burgess and De Toffoli 2022 — a self-citation by the first author). Human cognition was the coupling mechanism: intelligibility was not a separate requirement, it was a precondition of producing the certificate at all.

"But with AI, these two notions can now come apart dramatically. We can end up with formal proofs that float free from any intelligible proof."

They are careful that this cuts both ways, and the corpus should record the converse as well, because it is the case for formalization: "An intelligible mathematical argument can convey a grand idea while failing to establish that the result is actually true." Their two examples are the canonical ones — Jaffe and Quinn (1993) on Thurston's geometrization theorem for Haken three-manifolds, where a major insight with insufficiently complete proofs could become "a roadblock rather than an inspiration," and Hales's Flyspeck project (Hales et al. 2009), whose motivation was to check that the intelligible but unreviewable Kepler-conjecture proof really was one. So the claim is not anti-formal. It is that each notion alone is a roadblock, and that AI is the first thing that can supply one without the other.

What this contests in the corpus: the filter framing#

AI-Driven Formal Proof Search is built on DeepMind's line that "formal verification can serve as a filter for determining which proofs merit human review." De Toffoli and Duede's distinction is a direct objection to that framing's sufficiency, and it is worth stating precisely: the kernel filters for logical validity, and intelligibility is not a property it can rank. A sorry-free, axiom-clean Lean proof of a target and a five-line mathlib rewrite are the same kind of object to the compiler. What "merits human review" on the filter's own criterion is everything that compiled, ordered by nothing.

This is the second blind spot that page has now recorded in the same filter. The first, from ProofEvolve, was statement provenance — the kernel triages proofs perfectly and says nothing about whether the theorem was already in the training library, which fell back on five LLM judges and removed 25.6% of an evaluation set. The second is intelligibility. Both are cases of the same shape: the kernel answers exactly one question, and the questions it does not answer do not get easier because it answered that one.

The third property, across the kernel-versus-council axis#

Many-Agent Proof Harnesses frames 2026-09's two branches as kernel versus council: Lean accepts a .lean file, or a population of LLM falsifiers and a global verifier accepts a LaTeX document. De Toffoli and Duede's axis is orthogonal to that one, and neither branch sits well on it:

	checks logical validity	checks intelligibility
Lean kernel	yes, soundly	no — by construction; the check "does not itself require understanding"
LLM falsifier council	approximately — a model's opinion about validity	no — a model's opinion about validity, again
Human referee	slowly, fallibly	yes — this is the property the institution exists to test

One qualification on the table's top-left cell, added 2026-08. "Lean kernel — checks logical validity, yes, soundly" is true of the kernel and not automatically true of the harness that speaks for it. Kernel-Level Proof Auditing measures the gap: an evaluation server that compiles the file and greps the source for a sorry token — the check most LLM prover papers actually run — accepts declarations that depend on sorryAx, at a 31–44% rate for one released prover on PutnamBench. That does not move the logical/intelligible axis by an inch; the kernel was right the whole time and the stronger question (#print axioms, three-axiom whitelist) recovers the right answer. It does mean the row should read "yes, soundly — if you ask it the right question", which matters for this page because the argument here concedes the logical column completely in order to contest the intelligible one. The concession is safe; the reporting of it sometimes is not.

The council branch is the one this most complicates. Its artifacts look intelligible — natural-language LaTeX, 46- and 75-page proof drafts — but what its verifier is approximating is still deductive validity, not the "grasp, communicate, connect, build on" property. Producing prose is not the same as producing understanding, and nothing in that pipeline is scored on the difference. Read together with the kernel branch, the field has two mechanized answers to the logical question and zero instruments of any kind for the intelligible one.

The corpus's own evidence that the notions have already separated#

The argument is unmeasured, but three things already in the wiki are instances of exactly the gap it describes, and they are worth reading as such:

FrontierMath Erdős Benchmark — Erdős problem 90. An 18-page natural-language proof and a 1.2-million-line Lean formalization of the same result, produced by different parties. One of those artifacts is what a mathematician reads; the other is what the kernel accepts. This is the sharpest available illustration that "the proof" is now routinely two objects, and De Toffoli and Duede's point is that only one of them can do the job the discipline wants.
Automated Conjecturing — 6,522 statements, none proved. The AutoGraphForge run's novelty filter certifies that its survivors are not implied by a table of 559 classical relations. That is a logical property, decided by linear program. Whether any of them is interesting — the page's own #oq/now — is the intelligibility question in its generating form, and the filter cannot touch it.
OEIS Open Benchmark — 100 certified proofs, narrated by a model. Appendix A.1 of OEIS Open: How many conjectures can language models turn into theorems? (Epoch AI, empirical) tabulates the 100 costliest of 153 resolved open conjectures, and its sequence descriptions, conjecture statements and proof summaries "were written by GPT-5.6 Sol agents" given the accepted Lean proof, the OEIS entry and sandboxed access to the Mathlib source tree. No human check on the summaries is reported. So the intelligible half of each of those 100 results exists, is legible, and is uncertified — produced by exactly the machinery the kernel was brought in to replace, sitting on top of the object the kernel certified. This is not a flaw in the benchmark (the verdicts are unaffected by the prose), and it is the most concrete form the gap has taken in this corpus: not an absence of understanding but a generated stand-in for it, one whose fidelity to the certified artifact is guaranteed only by the fact that a model was shown the file. It is also a warning about the shape of the fix — the cheapest way to make a formal corpus readable is to have a model read it back, and nothing in that loop checks whether the story is the proof.
The Navier–Stokes AI Claim — the claim itself. OpenAI publishes a Lean formalization claim, a manuscript, agent counts and token totals, and no account of what makes the theorem true that a mathematician can use. De Toffoli and Duede's verdict is deliberately provisional: "Perhaps, we will find that they have [delivered a fruitful solution], but at the moment, the situation is far from clear." A third gap surfaced a week later, orthogonal to both notions of proof: Scientific American reports (Did OpenAI solve the wrong Navier-Stokes problem?, practitioner-opinion, wording as reported) that the theorem is valid for Clay's forced option "C" but is not the unforced problem mathematicians meant. That is fidelity of the statement to the question, which neither a kernel nor intelligibility addresses; see The Navier–Stokes AI Claim.

The strongest counter-evidence, and where it meets the objection (moved from AI-Driven Formal Proof Search, 2026-09-29). DeepMind's formal-proof-search paper (Advancing Mathematics Research with AI-Driven Formal Proof Search) reports that collaborators' understanding was enhanced by proof attempts even when the agent failed, because formal sketches let experts focus on the unresolved subgoals. That observation is about the collaboration: a human working an unsolved sketch learns from the attempt. De Toffoli and Duede's objection is about the artifact: a finished certificate no one had to understand to produce, from which no one can extract why the theorem is true. Both can hold. The process can enlighten the mathematician in the loop while the output stays unintelligible to everyone outside it. What would settle the tension is a case where the product, not the partnership, taught the field something, and neither source has one.

The second argument: "solving math" is not solving problems#

The post rejects two assumptions, and the intelligibility distinction only disposes of the first. The second is "mathematics is only about solving problems," and they attack it independently — because, they concede, "future AI systems are likely to produce genuine proofs that are at once formally certified and fully intelligible to mathematicians," at which point the first argument runs out.

Their case is that the game framing fails at the root: "there is no winner… There is no mathematical checkmate," so the Deep Blue–Kasparov comparison (Tristan Buckmaster's phrase, quoted in the post) has no referent. They endorse Jeremy Avigad's framing instead — "AI is nothing more than technology, designed to serve our purposes… when we drive a car, we aren't competing to see who can go faster" — and cite Tao's own 2026 list of mathematics' goals beyond problem solving: developing new theories and techniques, understanding the world, sustaining a community, training the next generation, contributing to cumulative knowledge, and creating works of aesthetic value. Their key move is that these were positively correlated with genuine solutions, and "AI breaks that correlation, for the same reason it separates the two notions of proof." They anticipate the obvious objection: "This is not moving the goalposts but recognizing that any specific goalpost is inadequate."

The benchmarkability warning#

One line is a direct claim about evaluation practice and belongs on this wiki more than the philosophy does:

"If mathematical success comes to be identified too closely with the production of certified answers, mathematics risks adapting itself to precisely those features that are easiest to benchmark and automate away."

That is Goodhart aimed at a discipline rather than a metric, and it is the standing risk under every scored open-problem denominator — see FrontierMath Erdős Benchmark, whose whole contribution is a fixed-budget denominator on curated open problems. The post reports that the concern is institutional, not only philosophical: a declaration at mathandai.org, initially signed by 25 Fields Medallists, warns of a "severe misalignment" between the goals of AI companies and those of the mathematical community. The authors' own diagnosis points inward too — "Mathematicians need to do more to examine their norms" — and they route it through David Bessis's argument that mathematics' credit economy needs rethinking.

Evidence note#

practitioner-opinion, and the tier is right. There is no measurement in the post, no data, no protocol, and the authors do not claim otherwise. What it supplies is a distinction and two arguments — which is why it can sharpen questions on other pages and settle almost none of them. Weigh it below every empirical source in this domain on any question of fact, and above the vendor-claim it responds to on the question it is actually competent on: what a certificate is evidence of.

Standing and conflicts. De Toffoli works on the philosophy of mathematical practice and the epistemology of proof; Duede on the epistemology of AI in science. Neither has a lab affiliation or a result at stake, which is the unusual and useful thing about the source — of the six documents in this compile batch, it is the only one whose author is not also the producer or the grader of the system under discussion. Against that: one of the two supporting citations for the historical claim (Burgess and De Toffoli 2022) is the first author's own, the venue is a blog rather than a refereed one, and Tao's introductory note says the post "was initially written in a different file format and converted using AI." The authors state that "an extended version of this text will appear elsewhere," so the peer-reviewed version is a future trigger.

Connections#

OEIS Open Benchmark — the gap's cheapest workaround, observed: 100 kernel-certified proofs whose only human-readable account is an unchecked GPT-5.6 Sol narration of the Lean file. A generated stand-in for intelligibility rather than an absence of it, and the first instance in the corpus of the distinction appearing inside a paper that gets everything else right
AI-Driven Formal Proof Search — the page whose organizing framing ("verification as a filter for determining which proofs merit human review") this post contests: the filter ranks logical validity and is blind to intelligibility, which is the second named blind spot in the same filter
The Navier–Stokes AI Claim — the occasion for the post and its running example; the argument is that even a clean repository would establish the logical half only
Many-Agent Proof Harnesses — the kernel-versus-council axis this distinction cuts across; the council branch produces prose without producing understanding, and is scored on neither
Automated Conjecturing — the same distinction on the generating side: "not implied by a table of 559 relations" is a logical certificate of novelty, and the interestingness question it leaves open is the intelligibility question before any proof exists
FrontierMath Erdős Benchmark — the corpus's cleanest instance of one result existing as two artifacts (18 pages / 1.2M lines), and the benchmark the "easiest to benchmark" warning aims at
Transformative Creativity — the answers/solutions line runs parallel to Boden's level-2/level-3 line: a certified answer is a search result inside a fixed space, a fruitful solution is what changes the space others work in
Outsource Your Thinking, Not Your Understanding — the same residue named in software: the machine can do the thinking and cannot do your understanding. This is the mathematical instance, with the twist that the formal certificate makes the understanding gap invisible rather than merely unaddressed
The Verifiability Thesis — math+Lean is the thesis's maximal case, and this is the argument that maximal verifiability still leaves the discipline's central good unproduced
Verification as the New Bottleneck (hub) — what a passing check does not certify, in the one domain where the check is sound
Lean — the tool the post credits precisely and bounds precisely: it "meets these standards exactly" and secures certainty, and certainty is not the whole of what a proof is for
Terence Tao — the host, and the source of the goals-of-mathematics list the second argument rests on
Kernel-Level Proof Auditing — the qualification on this page's "yes, soundly" cell: the kernel's verdict and the harness's summary of it are different objects, and the corpus's first measured false-accept rate separates them
OpenAI — the claimant whose announcement the post responds to
Statement Drift — the property between validity and intelligibility: whether the certified statement is the intended one. The Navier–Stokes forcing dispute is its spec-level case
Autonomous Scientific Discovery — where the Leiden Declaration now lives: a mathematicians' community statement on AI risks to "correctness, rigour, and standards of proof," the institutional counterpart of this distinction

Open Questions#

Is intelligibility operationalizable at all, or does it stay a philosopher's distinction? The falsifiable form: does anyone publish a protocol that tests whether mathematicians can state what makes the theorem true after reading a machine-produced proof — as opposed to checking that it is true — and does any machine proof pass it? Without such an instrument the distinction can sharpen claims but never settle one.
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? The corpus holds one case with both halves (Erdős problem 90, 18 pages against 1.2 million lines) and answers this nowhere.
De Toffoli and Duede concede the first argument has a shelf life: future systems are "likely to produce genuine proofs that are at once formally certified and fully intelligible." (Trigger event: the first machine-produced resolution of an open problem that working mathematicians publicly describe as having taught them why the result is true — a review, a survey, or an expository follow-up, not a correctness confirmation.)

Sources#

After Math — Silvia De Toffoli (University School for Advanced Studies IUSS Pavia) and Eamon Duede (Princeton University and Purdue University), "After Math", guest post on Terence Tao's blog (terrytao.wordpress.com), published 2026-09-12, ~2,000 words, practitioner-opinion — a philosophical argument with no measurements, no data and no protocol; the tier is as ingested and the full read confirms it. A web article, not PDF-derived, so no docling: table rules apply; no images and no tables in the source (the raw's provenance note records zero <img> tags in the post-content div), and the staged body is the full post-content element bounded at the sharing widget. Three sections — "Not All Answers Are Solutions", "You Need More than Solutions to 'Solve Math'", "Aftermath" — preserved from <b> pseudo-headings. Citations are inline hyperlinks, not a bibliography, and are used here as the authors use them (Thurston 1994; Jaffe and Quinn 1993; Hales et al. 2009; Burgess and De Toffoli 2022; C. Thi Nguyen 2019; Avigad 2026 on proofsandprompts.com; Tao 2026, arXiv 2608.16753; the Clay Institute's Navier–Stokes page; Buckmaster's statement PDF; the mathandai.org declaration; David Bessis's Substack). None of these was fetched — every one of them is a claim about a document this corpus does not hold, and is attributed in-text as the authors' reading of it. Editorial framing separated: the opening italic paragraph is Tao's own introduction of the guest authors (it ends "— T.") and includes his note that the post "was initially written in a different file format and converted using AI"; it is not part of the guest post's argument and is cited only as the host's framing.
OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), arXiv 2608.11941, 2026-08-12, 27pp, empirical. Cited here for exactly one sentence, from the Appendix A.1 preamble and quoted from prose reconciled against pdftotext -layout: that Table 1's sequence descriptions, conjecture statements and proof summaries "were written by GPT-5.6 Sol agents given the accepted Lean proof, the sequence's OEIS entry, and sandboxed access to the Mathlib source tree." The paper makes no intelligibility claim and does not discuss this distinction — the reading is this wiki's. No individual table row is cited anywhere. Full treatment on OEIS Open Benchmark
Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing — Vamshi & Yang (University of Maryland), arXiv 2608.28639, 2026-08-11, empirical. Cited here for a single qualification on the kernel column of the table above — the measured gap between the kernel's verdict and a compile-plus-sorry-scan harness's summary of it. It makes no argument about intelligibility and none of its numbers bear on this page's subject. Full treatment on Kernel-Level Proof Auditing
Advancing Mathematics Research with AI-Driven Formal Proof Search — Google DeepMind (AlphaProof Nexus, arXiv 2605.22763). Cited only for the collaborators' report that failed proof attempts still deepened their understanding.