When an AI Mathematician Tries to Write a Proof, Who Verifies It?

Who verifies an AI-written proof? Right now, the honest answer is: almost nobody, and the artifacts arriving in public repositories make that plain. Three recent GitHub projects release AI-generated mathematical proofs and formalizations, and every claim behind them is self-reported: the repositories describe their own provenance. None of the three records an expert having verified or refuted the released proofs.

That gap is now expensive. Per Wikipedia’s arXiv entry, in May 2026 arXiv’s computer science chair Thomas Dietterich announced that submissions showing “incontrovertible evidence” of unchecked LLM output face a one-year submission ban, with the author’s next submission requiring prior acceptance at a peer-reviewed venue. So the question in the title is no longer philosophical. It is an operational decision every reviewer, editor, and citing author now faces, and this article’s answer is a two-gate standard: an AI-assisted mathematical claim is citable when a full-result proof-assistant certificate compiles against the stated claim, or when an independent domain specialist attests to correctness. Prose, however fluent, fails both gates.

The artifacts are already here

The clearest example of the new artifact shape is the hodge-odd-fermat-fourfolds repository, which claims a proof of the rational Hodge conjecture for odd-degree Fermat fourfolds. Its README states that the manuscript, the reduction strategy, and the finite certificates were produced by AI systems (OpenAI Codex agents and GPT-family models) working over several weeks under the direction of Hongmin Li. The author then writes the sentence that defines this whole problem class: “I am not a specialist in algebraic cycles or Hodge theory, and I cannot independently vouch for the correctness of the proof. I am releasing it precisely for that reason: the mathematics either stands or it does not, and only human experts in this area can tell.”

This is a trust transfer, stated outright. The generator produced the argument, the director cannot check it, and correctness is delegated to an unspecified pool of domain experts who did not ask for the job.

The pattern is not a one-off. The same author’s valley-delta-low-t repository claims the t^1 and t^2 coefficients of the Valley Delta conjecture and Gillespie-Griffin Conjecture 7.3, again with an AI-generated manuscript, an AI-generated recurrence strategy, and Lean 4 certificates, and again with the disclaimer that the author “cannot independently vouch for the correctness of the proof.” Same structure, different field. That repetition matters: it suggests a recurring artifact class, not an anomaly.

The third artifact sits at the opposite pole. The lean-vector-balancing project describes itself as “generated almost entirely autonomously by ChatGPT 6 to formalise the results of the paper Reverse Littlewood–Offord problems with parity conditions” (arXiv 2510.05044), with the preamble as the only human-written text. Here the review question is different. The underlying paper already exists, so the question is not “is the theorem true” but “does this formalization faithfully encode that paper’s results.” That is a narrower, more tractable question, and it does not turn on the paper’s publication status, which the repository does not state. It also demonstrates something important: full proof-assistant formalization of a real paper is technically achievable today, at least as a self-reported claim.

What the concepts paper actually argues

The generation-side framing comes from a preprint essay, Machine Learning and Information Theory Concepts towards an AI Mathematician, which is worth stating precisely because it is easy to overread. The essay argues that current deep learning systems are “fairly good at capturing what psychologists (Kahneman, 2011) call system 1 or intuitive abilities, while they are weaker at system 2 or deliberate reasoning abilities.” Deliberate, multi-step, check-each-inference reasoning is exactly what proof-writing demands. So the literature that motivates AI mathematicians simultaneously predicts their outputs will be plausible but unsound: fluent system 1 pattern-matching dressed in the syntax of system 2 argument.

The paper also proposes two evaluators that reviewers can borrow directly, and this is its most useful contribution for practice:

• Compression-based usefulness: a new theorem counts as useful to the extent that the set of previous theorems plus the new theorem efficiently compresses the set of all provable mathematical statements. In principle, this gives a quantitative target for whether a claimed result matters.
• Held-out provability prediction: a held-out subset of mathlib, the Lean mathematical library, as a benchmark for whether a model can predict if a statement is provable before attempting the proof.

Both are proposals from a preprint essay, not deployed tools. But they sharpen the review question. A system that cannot predict provability better than chance on held-out mathlib statements has no business generating conjecture resolutions that specialists must then triage.

Partial certificates are the trap

All three repositories involve Lean 4, and it would be easy to treat “there is Lean code in the repo” as verification. The details in the READMEs say otherwise, and the distinction is the single most consequential thing a reviewer can learn from these three repositories.

The Hodge-fragment repository ships CI-checked Lean 4 certificates, but they cover the finite endpoints of the argument, not the reduction strategy that constitutes the mathematical heart of the proof. The Valley Delta repository similarly provides Lean 4 certificates for finite kernel identities, while the recurrence strategy lives only in machine-generated prose. In both cases, the load-bearing inference, the part a specialist would actually scrutinize, is unformalized. The certificates verify that specific finite computations check out; they do not verify that those computations establish the claimed theorem.

The vector-balancing project shows what the stronger pole looks like: a complete formalization targeting an existing paper, where the type-checker sees the whole argument rather than its endpoints. Even there, a compiling proof verifies the formalization as stated, not that the formalization faithfully captures the informal mathematical claim. Specification gaps, where the Lean statement subtly fails to match the theorem a reader thinks was proved, remain possible in any formalization, human or machine.

One scope caution: expect headlines along the lines of “AI proved the Hodge conjecture.” The repository covers the rational Hodge conjecture for a specific family of varieties, odd-degree Fermat fourfolds, and even that restricted claim is unverified. Novelty has its own caveat: the README’s relation-to-prior-work section notes that Kang (Bull. Aust. Math. Soc. 93, 2016, Corollary 3.2) “states a stronger result — the generalized Hodge conjecture for Fermat varieties of dimensions three and four in arbitrary degree — via refined motivic dimension.” The manuscript treats that statement “as a precedent rather than an input” after identifying “a specific step in the product argument (Kang 2015, Proposition 2.2(iv)) that we were unable to confirm”, and the README adds: “We do not claim to have disproved Kang’s statement.” The certificate columns above are the antidote to that kind of drift.

A checklist for any “AI did math” claim

The evidence supports a reusable evaluation instrument. Each axis below corresponds to something observed in the artifacts above, and each can be answered from a repository or manuscript in a few minutes.

1. Artifact completeness. Is there a full-result certificate in a proof assistant, a certificate covering only finite cases, or prose only? Only the first transfers trust mechanically. Finite-endpoint certificates verify computations, not the argument that makes those computations sufficient.
2. Vouching authority. Is correctness attested by an independent domain specialist, by the author (and is the author a specialist), or only by the generator? In both Li repositories, the author explicitly disclaims the ability to vouch. That disclosure is honest and useful, but it means the claim currently has no voucher at all.
3. Claim scope. Is this a novel theorem or a formalization of an existing result? The latter can be checked by comparing the formal statement to the statement in the source paper; the former requires full review of the argument.
4. Provenance disclosure. Is AI authorship declared? All three repositories declare it prominently, which is the good version of this. The policy risk below attaches to the undeclared version.
5. Statement fidelity. Even when a certificate compiles, does the formal statement match the informal claim? This needs a human who understands both, and it is the step that has no mechanical shortcut.

Applying the checklist: both Li manuscripts advance claimed-new results with partial certificates and no voucher, so they are unverified and should be treated as such in any citation or editorial decision. The two differ in claimed novelty: the Valley Delta repository points to open targets (“The Valley side is open”; Gillespie-Griffin proved only b = 2 and checked n ≤ 8), while the Hodge manuscript’s novelty is qualified by the Kang 2016 prior work noted above. The vector-balancing formalization passes the completeness axis, and the specialist its fidelity step calls for turns out to have a name: the repository sits in Lawrence Hollom’s GitHub account, and Hollom is the first author of arXiv 2510.05044. The README’s human check that the main results line up with the paper was therefore performed by the paper’s own author, which is the right person for statement fidelity and not an independent attestation of the paper’s mathematics. None of this is a judgment that the proofs are wrong. None of the three repositories reports an expert verdict either way. It is a judgment about what evidence exists.

What reviewers and venues are doing about it

Two responses are visible. The maximalist one is P2PCLAW, a project described in a Show HN thread, which proposes validating claims “through formal mathematical proof. Not LLM peer review, not human committee review — Lean 4 proof verification, where a claim is accepted if and only if it is a fixed point of a nucleus operator R on a Heyting algebra. The type-checker is the sole arbiter.” This is the logical endpoint of the trust-transfer problem: if humans cannot keep up with generated volume, remove humans from the loop entirely. Treat it as a live experiment, not a working institution. Its claims are self-reported via a launch post, including its report of technical dialogue with Harvard’s Zitnik Lab about verifying AI-generated drug interaction hypotheses; the launch post is the only source for that dialogue.

The institutional response is enforcement. The arXiv policy described on Wikipedia (a tertiary source, not the primary announcement) penalizes unchecked LLM output rather than LLM output as such. Note the gap: the Wikipedia summary never defines what counts as “checked.” A reviewer applying the checklist above would say checked means a full-result certificate or specialist attestation, but whether arXiv’s moderators apply anything like that standard is unknown. Authors should flag this ambiguity rather than assume their disclosure practices are safe. The practical exposure is concrete: a one-year submission ban, and a requirement that the next submission pass peer review elsewhere first.

The verdict and its limits

The two-gate standard: treat any AI-assisted mathematical claim as unverified until a full-result proof-assistant certificate compiles against the stated claim, or an independent domain specialist attests to correctness. Prose from a non-specialist author, however confident, fails the bar. Finite certificates verify what they cover and nothing more. If you are an editor, ask which gate the submission passes before sending it to referees. If you are a citing author, cite it as an unverified claim or do not cite it. If you are the human in the loop directing the AI, understand that “I released it for human verification” transfers labor to a reviewer pool that did not volunteer. On the receiving end, venues are pulling back intake: in November 2025 arXiv stopped accepting computer-science review articles and position papers not already vetted by a journal or conference, a step its Wikipedia entry attributes to “an increase in AI-generated research.”

Now the limits, because they are large. Everything decisive here is self-reported: the concepts paper is a preprint essay, the repositories describe their own provenance and certificate scope with no third-party validation, and neither Li repository records any specialist having verified or refuted either manuscript. The standard I am arguing for is an inference from those observations, not a measured finding; it is the minimum evidence that would transfer trust, given that partial certificates leave the load-bearing arguments unverifiable. Nothing here settles whether human review capacity can absorb AI-generated volume, whether P2PCLAW’s architecture works as described, or how arXiv will define “unchecked” in practice.

If there is a structural point worth holding onto, it is this: the capability-gap essay hypothesizes that current systems are strong at intuitive, system 1 generation and weaker at deliberate, system 2 reasoning, and the three artifacts are consistent with that gap. The economics, that generation is cheap while verification stays expensive, is my inference from the artifacts, not a claim the essay makes. Verification, not generation, is the bottleneck. Review culture has not yet priced that in, and the arXiv ban suggests venues are starting to.

Frequently Asked Questions

What is the two-gate standard for verifying AI-assisted mathematical claims?

an AI-assisted mathematical claim is citable when a full-result proof-assistant certificate compiles against the stated claim, or when an independent domain specialist attests to correctness. Prose, however fluent, fails both gates.

What penalty does arXiv impose for unchecked LLM output?

in May 2026 arXiv’s computer science chair Thomas Dietterich announced that submissions showing “incontrovertible evidence” of unchecked LLM output face a one-year submission ban, with the author’s next submission requiring prior acceptance at a peer-reviewed venue.

Why are finite-endpoint Lean certificates insufficient for verification?

The certificates verify that specific finite computations check out; they do not verify that those computations establish the claimed theorem.