An AI proof can pass—and still answer the wrong question

A computer can accept a proof of the wrong theorem. That does not necessarily mean the proof-checking software failed: it may have correctly checked a statement that an AI translated incorrectly from the researcher’s words. The calculation passes, but the original question remains unanswered.

In a November 2026 preprint, György Eigner, Patrik P. Süli and Roland Hollós propose a framework for making this problem visible. Their approach combines software checks, a separate comparison with the original claim, human decisions and a record of who contributed what. It is a methodology illustrated by a small example, not evidence that automated research checking has been solved.

Two different gaps

The authors distinguish three things: the claim in a paper, the computational object submitted for checking, and the software’s verdict. That computational object might be a formal theorem, a statistical script or a simulation model.

There are two gaps between them. One concerns whether the software correctly checks its input. The other concerns whether that input faithfully represents the researcher’s claim. A proof assistant addresses the former; accepting its proof does not automatically settle the latter.

Faithfulness can require preserving the objects, assumptions, scope and numerical details of a claim. In statistics, it includes the population, test and corrections for multiple comparisons. Checking whether an author’s particular argument works adds another requirement: proving the same conclusion by a different route is not enough.

Drawing on another preprint about translating mathematics into formal proofs, the authors argue that no algorithm can settle every such fidelity question. Their proposal does not overcome that limit. It aims to expose unresolved choices so a responsible human can decide them.

Freeze the question before checking it

The workflow starts by fixing the claims and acceptance conditions before any checking tool runs. Each tool then receives a fresh formulation derived from those frozen claims, rather than a translation of another tool’s code. This is intended to avoid copying one mistaken interpretation across several checks.

Each computational object also gets a literal description of what it checks. A calculation for a few examples must not be reported as a general proof. Numerical support must remain distinguishable from an exact result.

A separate fidelity audit would compare the original claims with the final computational objects, inspect omissions and changed assumptions, and record deviations. Humans would approve the starting targets, review interpretations, decide unresolved deviations and accept or reject the final conclusions.

The authors describe two implementations of the checking layer: one using Wolfram Language, MATLAB and the Lean proof assistant, and another using Python and R for statistics. These implementations produce material for an audit; they do not themselves complete the entire framework.

When 0.37 is both right and wrong

The mathematical demonstration used two short claims. One said that six divides n³ − n for every natural number n. The other said that the largest value of f(x) = x exp(−x), for nonnegative x, is 0.37.

That decimal creates a consequential ambiguity. Does it mean exactly 0.37, or a maximum rounded to two decimal places? Before checking, the system split the sentence into separate claims for those readings.

Wolfram Language and Lean established that the maximum is 1/e, attained at x = 1. Its value is approximately 0.36788. The exact-decimal claim was therefore refuted, while the rounded reading was confirmed.

MATLAB found the critical point and its value but did not establish the required global upper bound. Its results for both readings remained inconclusive. For the divisibility claim, its calculation checked six remainder cases, but the step explaining why those cases cover every natural number appeared in a code comment rather than a MATLAB-checked argument. The report flagged that limitation.

These differences matter: the workflow preserved unequal strengths of evidence rather than treating all successful computations as equivalent.

A demonstration, not a performance test

The example stopped after the tool-checking stage. The authors did not run the fidelity audit or the human–AI contribution report on it. The statistical implementation was described but not evaluated, and the study measured neither error-detection rates nor savings in human effort.

Another limitation is shared interpretation. The same AI writes formulations and back-translations in the implementation and would perform the audit. Different checking programs can therefore agree while inheriting the same misunderstanding.

The proposed contribution report would document consequential human and AI decisions without assigning an overall percentage of authorship. Its purpose is accountability, not a numerical measure of credit.

The central distinction remains useful even without a large evaluation: software acceptance is evidence about what was submitted. Establishing that it answers the intended research question is a separate task.