Proofs and Consequences: How Math Reveals What AI Still Doesn’t Know

TL;DR for operators

Mathematical proof is a nasty evaluation setting for AI systems because it leaves fewer hiding places. A model cannot merely land on a final number; it has to preserve the truth of each step. That is precisely why Guo et al.’s RFMDataset is useful: it tests whether advanced reasoning models can construct complete natural-language proofs, then classifies how they fail when they cannot.¹

The uncomfortable result is not that weaker models struggle. That would be Thursday. The uncomfortable result is that models marketed, used, or perceived as serious reasoners still produce invalid proofs at meaningful rates, including on relatively basic problems. In the paper’s main accuracy table, some models sit at or below roughly 15–25% overall proof accuracy under the primary judge, while the stronger rows reach around 56–66.5%, depending on the model. That is better, but not remotely the same as dependable.

The dominant failures are also operationally familiar: logical violations, hidden assumptions, vague arguments, and incomplete proofs. Translate out of mathematics and this becomes: the model makes an invalid inference, imports a premise you never supplied, waves at a gap, or stops before the job is actually done. A compliance memo, financial model explanation, engineering diagnosis, or scientific summary can fail in exactly these ways while still sounding calm and senior.

The paper’s self-reflection experiment is the part managers should read twice. Prompts that ask models to check logical steps or avoid vague arguments can improve some subsets. But the gains are modest relative to the number of remaining failures. “Tell the model to be rigorous” is not a control system. It is a sticky note on a machine that sometimes invents premises.

Cognaptus inference: treat LLM reasoning as a proposal generator, not a proof engine. For high-stakes workflows, the business value is not a longer chain-of-thought. It is a verification architecture: independent checkers, domain-specific adversarial examples, step-level validation, formal tools where possible, and human escalation when the model’s argument carries risk.

The scoreboard is not the story; the proof is

A familiar mistake in AI procurement is to treat benchmark performance as a general personality trait. The model scores well on a mathematical competition benchmark, therefore it is “good at reasoning”. The model explains itself in long paragraphs, therefore the explanation is probably reliable. The dashboard turns green, therefore the machine must have understood something.

The paper attacks exactly that inference.

The authors point out a structural weakness in many mathematical benchmarks: they often measure the final numerical answer. That is efficient, but it has a blind spot large enough to park a governance committee inside. A model can reach the right final answer through a flawed route, or fail in ways that a simple answer check cannot diagnose. Worse, if a benchmark has only a small number of problems, high accuracy leaves too few failures to study. A model scoring 90% on a 30-question benchmark gives researchers only three failures to inspect. That is not a failure-mode analysis. That is a post-mortem with three bodies and a very confident narrator.

Proof changes the evaluation object. A proof is not merely an answer; it is a chain of obligations. Each step has to follow from previous statements, valid assumptions, or established theorems. One invalid inference can break the whole argument. That makes proof a useful diagnostic environment for reasoning models, especially when the question is not “Can the model sometimes solve the task?” but “How does it fail when the reasoning matters?”

That distinction is the article’s core business relevance. Most enterprise tasks do not look like olympiad geometry. But many enterprise tasks do look like proof in one crucial respect: the answer is only as useful as the reasoning path behind it.

A tax analysis that assumes the wrong jurisdiction, a loan-risk assessment that silently imports a borrower attribute, a procurement recommendation that ignores a boundary condition, or an engineering diagnosis that declares a root cause from suggestive evidence—all of these are proof-like failures. The final paragraph may be fluent. The logic can still be broken.

RFMDataset turns reasoning into inspectable failure

RFMDataset contains 200 manually selected mathematical proof problems. The problems span middle-school, high-school, and undergraduate levels, with 52, 88, and 60 problems respectively. They also cover nine mathematical subject areas, including geometry, calculus, probability, algebra, number theory, combinatorics, trigonometry, set theory, and number sequences.

The important design decision is not just the number of questions. It is the dataset’s purpose. RFMDataset is not built mainly to crown the best model on another leaderboard. It is built to expose failure modes. That changes the selection logic.

The authors select for diversity, difficulty, and novelty. Diversity means the benchmark should not collapse into one narrow family of problems. Difficulty does not mean every item is olympiad-level; it means even easier questions should require careful reasoning rather than automatic pattern completion. Novelty means the dataset tries to avoid overused sources and benchmark contamination. Geometry questions are also reformulated so the scene can be reconstructed from text, and models are restricted from using certain coordinate or parametric shortcuts when those would dodge the intended geometric reasoning.

The evaluation pipeline has two layers. First, models generate natural-language proofs. Second, an LLM judge evaluates whether the proof is completely correct and classifies any errors into a fine-grained taxonomy. The primary judge is Gemini-2.5-pro-preview-0506. The authors then validate judge reliability with human evaluation on 240 sampled model answers, reporting an overall Matthews Correlation Coefficient of 87.61% between human labels and judge labels. That does not make the judge infallible, but it does make the measurement more credible than “we eyeballed it and felt scholarly”.

The taxonomy is the paper’s real instrument. It includes transformation error, over-generalisation, invalid construction, wrong division, circular reasoning, logic violation, hidden assumption, boundary neglect, vague argument, incomplete proof, and others.

A simplified operational translation looks like this:

That last category deserves special respect. Circular reasoning is the official mascot of many strategy decks.

The main results are low enough to change the procurement question

The paper’s headline empirical result is straightforward: many advanced models struggle to generate completely correct natural-language mathematical proofs.

Under the primary judge, Table 3 reports the following overall accuracies:

Two observations matter.

First, the weaker rows are not merely a little behind. Several widely known reasoning models fail most of the proof tasks. A model can be impressive in many contexts and still be unreliable when asked to produce a rigorous argument from premises to conclusion. These are not the same capability.

Second, even the better rows should not be casually rebranded as dependable proof engines. A 60–66.5% complete-proof accuracy rate may be an impressive research result. It is also a terrible control if the workflow requires correctness by default. Nobody wants a contract review, bridge-load calculation, or anti-money-laundering escalation process that is “directionally strong” two-thirds of the time. Unless the business model is litigation.

The paper also reports that model performance varies by mathematical domain. The models tend to perform worse in geometry, number sequences, combinatorics, and probability, while doing relatively better in algebra and number theory. This matters because it weakens a common managerial shortcut: “the model is good at math” is not a stable property. Method matters. Domain structure matters. The type of reasoning matters.

The same issue appears across difficulty. Accuracy generally declines as problems get harder, which is unsurprising. More interestingly, most models fail to reach 60% even on the lowest difficulty level, with only two Gemini variants clearing that threshold in the authors’ discussion. The paper is therefore not simply saying: “hard proofs are hard.” It is saying: “even basic proof obligations can expose cracks.”

The failures are boring, which is why they are dangerous

The most useful part of the paper is not the accuracy table. It is the failure distribution.

Across incorrect proofs, the dominant error categories are logical violation, hidden assumption, vague argument, and incomplete proof. The authors also report that this pattern is broadly similar across models and remains dominant across difficulty levels. In Appendix E.1, they examine whether failure modes shift with problem difficulty and find that the same four categories remain central, with logical violation, vague argument, and incomplete proof generally increasing with difficulty while hidden assumption slightly decreases.

That pattern should make operators uncomfortable. If failure modes were exotic, they could be handled as edge cases. Instead, they are foundational.

A logic violation means the model cannot preserve validity across a step. It may know the relevant objects, cite plausible principles, and still make a deduction that does not follow. In business workflows, this is the model that sees “sales increased after the campaign” and quietly turns it into “the campaign caused sales to increase”. It is not always wrong. That is the problem. It is plausible often enough to pass casual review.

A hidden assumption is even more insidious. The model uses a premise that was never supplied or proven. In mathematics, that might mean applying a theorem without establishing its conditions. In enterprise work, it might mean assuming a policy applies to a subsidiary, assuming a customer segment has a certain risk profile, or assuming data is complete because the spreadsheet has no empty rows. Hallucination is not only fake facts. Sometimes it is fake permission.

A vague argument is what happens when fluency substitutes for proof. The model says something is clear, natural, intuitive, or follows by standard reasoning. Sometimes that is acceptable; experts use compressed reasoning all the time. But in a proof benchmark, vagueness becomes measurable because the missing bridge matters. In business, vague arguments are dangerous because they are socially efficient. They sound like competence. They save time. They also bury risk.

Incomplete proof is the operational classic. The system answers half the question. It handles sufficiency but not necessity, the normal case but not the exception, the initial period but not the renewal clause, the happy path but not the failure state. Then it stops with a conclusion-shaped sentence. The fact that the prose has ended does not mean the reasoning has.

The paper’s value is that it converts these behaviours from vibes into categories. That is not glamorous, but it is exactly what evaluation needs. You cannot manage “the model sometimes reasons weirdly”. You can manage “the model frequently imports hidden assumptions under these task conditions”.

Long reasoning is not the same as reliable reasoning

One appendix result deserves more attention than it will probably get. The authors analyse whether longer chain-of-thought leads to better problem-solving performance across four models with publicly available reasoning traces. They report no clear correlation between reasoning-chain length and accuracy across domains, and observe that longer reasoning chains often correspond to lower accuracy.

This should not be overread. The paper does not prove that shorter reasoning is always better, nor that chain-of-thought is useless. It shows that length is not a reliable proxy for correctness in this setting.

That distinction is essential. Many AI interfaces have trained users to associate longer outputs with deeper thought. The model pauses, reasons, expands, reflects, and produces a long answer. The user experiences cognitive theatre. But proof does not reward theatrical depth. It rewards valid transitions.

There are at least two mechanisms that can explain the paper’s observation. One is error accumulation: more steps create more opportunities for a single invalid inference to poison the chain. Another is domain-method mismatch: if the model does not know the right proof technique, more tokens may simply mean a longer walk in the wrong forest.

The practical lesson is blunt. Do not buy reasoning length as a governance control. A longer explanation can be useful for review, but only if the review process checks the validity of its steps. Otherwise, it is just an audit trail of the model getting lost in higher resolution.

Self-reflection helps at the margin, not at the control layer

The authors test whether targeted self-reflection prompts can reduce failures. This is an intervention experiment, not the paper’s main evidence. Its purpose is to ask whether some errors are superficial generation flaws that can be corrected by telling the model to inspect itself more carefully.

They test three prompt variants on Doubao-1.5-thinking-pro, GPT-o4-mini, and Deepseek-R1-0528:

The results are mixed but informative. Doubao improves from 24.50% overall to 29.00% under the combined reflection prompt. GPT-o4-mini improves from 21.00% to 24.50% under logical reflection, though other reflection variants do not help as much. Deepseek-R1-0528 moves from 37.00% to 37.50% under the combined prompt, with some category-level improvements but limited overall movement.

The authors also compute a “Best” score that selects the best-performing reflection strategy across middle-school, high-school, and undergraduate subsets for each model. That produces higher synthetic scores: 31.50 for Doubao, 27.00 for GPT-o4-mini, and 42.00 for Deepseek-R1-0528. This is useful as an upper-bound diagnostic, but it is not a deployable strategy unless you already know which reflection prompt will work for which problem type. Conveniently knowing the optimal prompt in advance is a wonderful capability, usually found in hindsight and vendor demos.

The operational conclusion is not “reflection is useless”. It is more precise: reflection prompts can recover some performance, but they do not convert unreliable proof generation into dependable proof generation. The model can be instructed to look for logical violations and still miss them. It can be instructed to avoid vague arguments and still produce gaps. Internal self-correction remains part of the generation process; it is not an independent verifier.

That matters for enterprise AI design. Prompting the same model to check its own answer is cheap and sometimes worthwhile. But for high-stakes work, it should be treated as a first-pass improvement, not a safety boundary.

The appendix tests the measuring instrument, not a second thesis

The appendix is not decorative. It answers the obvious methodological objections.

First, the paper validates the judge. Human evaluation on 240 sampled answers produces high overall agreement with the primary LLM judge. The authors also include a failure case where the judge is too strict, labelling a proof incomplete because it relies on a reasonable theorem not explicitly derived from the problem statement. This is important. A strict proof judge can undercount acceptable proofs if it demands every bridge be rebuilt from first principles. The authors acknowledge that risk rather than pretending the judge descends from Mount Formalism carrying stone tablets.

Second, Appendix E.3 tests other LLM judges. The paper reports that GPT-5 and Gemini-2.5-pro-preview-0506 produce highly similar overall evaluations, while less capable judges are more lenient. This supports the credibility of the main evaluation, but it also reveals a deeper issue: evaluation itself is model-sensitive. If an organisation uses a weak model to judge another weak model, it may simply automate reassurance.

Third, the appendix explores failure modes by difficulty and chain-of-thought length. These are robustness and sensitivity checks. They do not replace the main findings, but they sharpen interpretation. The persistence of the four dominant failure modes across difficulty suggests the issue is not confined to unusually hard problems. The lack of clear correlation between reasoning length and accuracy weakens the idea that more verbal reasoning is inherently safer.

Finally, the authors propose two solution directions: high-quality domain-specific training data and agentic step-level interaction with formally verifiable environments such as Lean. The second is especially relevant. If the problem is unreliable single-step reasoning, then an external verifier can provide feedback that internal reflection cannot. The model proposes; the environment checks; the model revises. That is closer to an engineering loop than a monologue.

The business lesson is verification design, not benchmark tourism

The temptation after reading a paper like this is to ask which model won. That is the least interesting question.

The better question is: what type of control would have caught the failure?

For operators, this suggests five design principles.

First, separate generation from verification. The model that writes the answer should not be the only authority judging whether the answer is valid. Even when the same base model is reused, the verification process should be structured differently: different prompt, different evidence access, different scoring rubric, and ideally a stronger or specialised evaluator.

Second, evaluate the reasoning path, not just the final output. In many business workflows, the final answer is easy to approve when it matches expectation. That is exactly how hidden assumptions survive. A workflow that recommends “approve”, “reject”, or “escalate” should be tested on whether its intermediate grounds are valid, not merely whether the final label matches historical decisions.

Third, build domain-specific failure taxonomies. RFMDataset’s categories are mathematical, but the pattern generalises. Legal review might track missing jurisdiction, unsupported interpretation, clause omission, circular risk justification, and boundary-condition neglect. Finance might track causal overreach, stale-data dependence, unsupported assumptions, scenario incompleteness, and metric substitution. Engineering might track unverified root cause, ignored edge case, invalid constraint, and incomplete remediation.

Fourth, use adversarially selected examples. Random test sets are useful for broad coverage, but failure-mode discovery needs examples that force the system to expose its habits. RFMDataset intentionally selects proof tasks that require careful reasoning. Enterprises should do the same with their own workflows: collect cases where shallow pattern matching is likely to look convincing and be wrong.

Fifth, formalise where possible and escalate where not. Some claims can be checked with tools: arithmetic, code execution, database queries, policy rules, unit constraints, schema validation, theorem provers, simulation environments. Other claims require expert judgement. The boundary should be explicit. The worst design is the grey zone where a model gives a confident explanation and everyone quietly decides that sounds like governance.

Boundaries: proof is a sharp test, not the whole world

The paper’s limitations matter.

RFMDataset has 200 problems. That is large enough for the paper’s diagnostic purpose and comparable to some proof benchmarks, but it is not a census of mathematical reasoning. The exact accuracy numbers should not be treated as universal constants. A model’s score on this dataset is not its score on every proof task, let alone every enterprise reasoning task.

The benchmark uses natural-language proofs. That is useful because most current LLM deployments operate in natural language, not Lean or Coq. But natural language also creates ambiguity. A proof can be compressed in ways that are acceptable to experts but difficult for an automated judge to assess. The authors’ own judge-failure example shows that strictness can become a measurement issue.

The evaluation uses pass@1 rather than pass@k. This suits the failure-mode analysis because a single sample produces enough failures to classify, and multiple generations are costly. But it means the results measure first-attempt proof reliability, not the best proof a model might eventually produce after repeated sampling, search, tool use, or human feedback.

The business translation also has limits. A mathematical proof has a clear standard of correctness. Many enterprise tasks do not. Strategic analysis, market entry, hiring, customer segmentation, and product prioritisation often involve uncertain judgement rather than proof. In those contexts, the lesson is not to demand theorem-level certainty. The lesson is to identify which parts of the reasoning are checkable, which assumptions are imported, and which conclusions are being presented more strongly than the evidence permits.

So no, this paper does not prove that LLMs are useless for reasoning. That would be a lazy reading, and laziness already has enough automation. It shows that reasoning output can be structurally unsound even when produced by advanced models, and that the failure modes are specific enough to measure.

Conclusion: audit the chain, not just the answer

The paper’s central contribution is not that it found another benchmark where models look worse. The field has enough leaderboards to tile a bathroom. Its contribution is diagnostic: it uses natural-language mathematical proof to reveal how reasoning breaks.

The result is a useful correction to the current mythology of reasoning models. High performance on answer-based mathematical benchmarks does not guarantee rigorous proof. Long chain-of-thought does not guarantee validity. Self-reflection prompts do not guarantee repair. Stronger models help, but they do not remove the need for verification.

For business users, the practical lesson is simple and mildly inconvenient: if correctness matters, build systems that can catch bad reasoning. The model should not merely answer. It should expose claims, identify assumptions, connect evidence, submit intermediate steps to checks, and know when an external verifier or human expert must take over.

That is less glamorous than a single omniscient agent. It is also how serious systems are built.

The future of enterprise reasoning is not the longest monologue. It is the shortest trustworthy path from claim to checked evidence.

Cognaptus: Automate the Present, Incubate the Future.