When Less Proves More: The Case for Minimalist AI Theorem Provers

Proof is a good place to test AI humility.

In ordinary business writing, a model can sound confident, cite familiar patterns, and still be quietly wrong. The error may not surface until the contract is signed, the policy memo is circulated, or the spreadsheet has already acquired the authority of a sacred object. In formal theorem proving, the arrangement is less polite. The model writes code. Lean compiles it. The compiler either accepts the proof or sends it back covered in red ink.

That makes theorem proving unusually useful for studying AI agents. Not because every business problem should be converted into Lean code — please do not ask your sales team to formalize the pipeline in dependent type theory before lunch — but because theorem proving gives us a clean version of a broader design question:

What happens when an AI system is forced to improve through verified feedback rather than vibes?

The paper A Minimal Agent for Automated Theorem Proving introduces AxProverBase, a deliberately simple theorem-proving agent built around that question.¹ The result is not another maximalist agent diagram with seven subagents, twelve arrows, and the usual promise that autonomy will arrive after one more orchestration layer. The system has three core ingredients: iterative Lean feedback, compact memory, and lightweight search. With that scaffold, a frontier general-purpose model becomes surprisingly competitive with more specialized and more elaborate theorem-proving systems.

The interesting part is not merely that the system performs well. It is how little machinery is needed before performance starts to look serious.

The mechanism is a loop, not a monument

AxProverBase is built around a simple cycle.

A proposer agent receives a Lean theorem and attempts to write the proof. Lean checks whether the proposed code compiles and whether it actually closes the theorem without forbidden shortcuts such as sorry, admit, extra axioms, or suggestion tactics. If the proof fails, the system sends feedback into a memory module. The proposer then tries again, now informed by what went wrong before. If the proof appears to compile, an additional reviewer agent checks that the theorem statement has not been quietly altered and that the result is not exploiting a loophole.

That sounds almost disappointingly plain. Good. Disappointing simplicity is often where engineering starts becoming useful.

The paper’s point is not that a single Lean compiler message magically teaches mathematics. The mechanism is more specific. Compiler feedback converts failure into a structured diagnostic signal. A memory mechanism prevents the agent from rediscovering the same mistake every five minutes, which is also a useful feature in humans. Search tools help the agent find the right Mathlib names, imports, and proof tactics when its internal memory of the Lean ecosystem is stale or hallucinated.

The architecture can be summarized as follows:

This is a mechanism-first story. The benchmark table matters, but it should come after the reader understands what is being tested. Otherwise, the result degenerates into the usual leaderboard ritual: number, applause, caveat, repeat.

The biggest gain comes from being allowed to fail usefully

The paper’s bottom-up ablation study is the most important evidence because it asks the right question: which part of the agent actually matters?

The authors evaluate component additions on a randomly selected 100-sample subset of PutnamBench. That detail matters. The ablation subset is not the final benchmark result; it is a controlled testbed for understanding the system. In editorial terms: this is mechanism evidence, not a victory parade.

The first baseline is single-shot proof generation. A general-purpose model writes a proof, receives no feedback, and never gets a second chance. This is the familiar “prompt harder” approach to AI reliability. It can work on easy cases, but the paper finds it sample-inefficient. Generating more independent proofs helps only slowly because difficult theorems remain difficult across samples.

Iterative refinement changes the economics of failure. Instead of treating each attempt as a fresh lottery ticket, the system lets the model see why the previous attempt failed. This produces the largest performance gain among the architectural components.

That is the first lesson for business AI systems: the opposite of hallucination is not necessarily a larger model. Often, it is a better failure channel.

A model asked to “write a compliant answer” is guessing inside a fog. A model that receives deterministic feedback — “this clause conflicts with policy X,” “this calculation does not reconcile,” “this API call fails schema validation,” “this proof leaves these goals unsolved” — can perform repair rather than improvisation. The important shift is from generation to controlled iteration.

Memory is not chat history with better branding

The second major contribution is the memory comparison.

AxProverBase tests two memory designs. One simply passes along the history of recent proof attempts. The other uses a self-managed context, where a memory module condenses key lessons from previous attempts into a compact note for the proposer. The paper reports that self-managed context performs better: it proves on average 7% more theorems, costs 20% less overall, costs 10% less for an equal number of iterations, and has roughly half the dispersion between runs.

That is a useful result because many agent systems still confuse memory with transcript accumulation. Keeping the last five attempts is easy. It is also crude. The prompt grows, irrelevant details remain, and the model may spend context budget rereading its own failed reasoning with the solemnity of an archive clerk.

Self-managed memory does something more practical. It asks: what should survive from the last failure into the next attempt?

In theorem proving, the answer might be a lemma that did not exist, an import that failed, a tactic that produced the wrong subgoal, or a proof decomposition that seemed promising. In business workflows, the equivalent might be a rejected invoice rule, a recurring data-cleaning exception, a legal clause that compliance repeatedly flags, or a customer-support escalation pattern.

The business interpretation is not “add memory to your agent.” That phrase is nearly empty. The interpretation is: compress operational experience into a reusable, task-facing form that changes the next action.

A memory system earns its keep only when it reduces repeated failure. Otherwise it is just a diary with token costs.

Search helps, but it is not the main character

Search tools improve AxProverBase, but the paper is careful about magnitude. The authors add LeanSearch for Mathlib retrieval and Tavily web search for practical proof-strategy discovery. The full system performs best with search, yet the improvement is smaller than the gains from iterative feedback and memory.

This is a useful correction to a common agent-design reflex. When an AI workflow underperforms, the immediate temptation is to bolt on retrieval. Retrieval is visible. It feels concrete. It gives the demo something to show.

But in AxProverBase, search is not the foundation. It is a friction reducer.

The paper’s error analysis explains why. Many proof failures involve misidentifying or misusing Lean and Mathlib objects. Search helps reduce those low-level struggles. But the larger transformation comes when the system stops wasting iterations on syntax, bad names, and missing imports, and starts spending more effort on open proof goals.

That distinction matters outside theorem proving. Retrieval is most valuable when the bottleneck is missing or stale context. It is less valuable when the bottleneck is poor task decomposition, weak validation, or repeated unlearned failure. In those cases, retrieval only gives the model more material with which to be confidently unhelpful. A familiar product feature, admittedly.

The error analysis is more revealing than the headline score

The appendix error analysis deserves more attention than the typical reader will give it.

The authors classify failed proof attempts into categories such as bad imports, name errors, remaining sorry, syntax errors, tactic failures, and unsolved goals. These categories are not merely labels. They indicate how far the proof attempt got before failing.

A bad import or syntax error is a shallow failure. Lean cannot even reach meaningful proof checking. An unsolved goal is a deeper failure. The surrounding code is coherent enough for Lean to understand the proof state, but the proof has not yet closed the theorem.

That means a rising share of unsolved-goal errors can actually be a sign of progress. The system is failing later and more informatively.

The paper reports that architectural improvements shift the error distribution away from lower-level errors and toward higher-level proof-state failures. Name errors drop from 13% to 7%; in absolute terms, name errors fall by 53% and syntax errors by 26% between the feedback-only system and the full system. Meanwhile, unsolved goals rise from 27% to 36% as a share of errors, while their absolute count changes little.

This is an important diagnostic pattern: the system is not simply making fewer mistakes. It is making better mistakes.

For business AI, that is a powerful evaluation lens. A workflow that fails because it cannot parse a document, match a schema, or call the correct API is different from a workflow that reaches the hard judgment boundary and asks for human review. Both are failures. They do not mean the same thing.

A serious AI operations dashboard should therefore track not only success rate, but failure depth.

The operational target is not to eliminate every failure. That is brochure logic. The target is to push failures toward the layer where diagnosis is meaningful and intervention is cheap.

Stronger models benefit more from the scaffold

The foundation model comparison adds another layer to the story.

In single-shot mode, the tested models look relatively similar, with pass@20 around 5% in the paper’s comparison. Once embedded inside the AxProverBase scaffold, the differences widen. Stronger models benefit more from feedback, memory, and tools. Claude Sonnet 4.5 and Claude Opus 4.5 outperform Gemini models by a large margin in this setting, and the error traces reveal a practical reason: Gemini models frequently use older or hallucinated Lean and Mathlib imports despite the prompt specifying the version and despite search access.

The appendix quantifies this sharply. Bad imports account for 56% of failed proof attempts for Gemini 3 Flash and 33% for Gemini 3 Pro, compared with about 1% for Claude Sonnet 4.5 and 0.4% for Claude Opus 4.5.

This is not a generic “Model A beats Model B” point. Model rankings change. Product teams should not build strategy around one frozen leaderboard, unless they enjoy archaeological work.

The more durable point is that scaffolding amplifies capabilities unevenly. A strong agent framework does not automatically rescue a model whose failures occur at the wrong layer. If the model burns iteration budget on bad imports, the proof loop cannot spend enough time on mathematical progress. In business workflows, the same pattern appears when an agent repeatedly fails at file handling, database field names, or basic policy references. The validator may be excellent, but the workflow still leaks time before reaching the real problem.

Better scaffolding is not a substitute for model competence. It is a multiplier. Multipliers are awkward when the base number is small.

The benchmark results are strong, but their meaning is specific

The final benchmark evaluation uses Claude Opus 4.5 with a 32k thinking budget and 50 iterations. AxProverBase reaches:

The PutnamBench result is especially interesting because AxProverBase nearly matches Hilbert’s reported pass@1 result: 54.7% versus 55.9%. Hilbert is a more complex recursive prover that uses informal reasoning, theorem retrieval, specialized Lean proof generation, verifier feedback, and subgoal decomposition. AxProverBase gets close with a much simpler setup.

The cost-performance appendix sharpens the comparison. On PutnamBench, AxProverBase reaches its 54.7% result with 4.2 million maximum tokens per problem and 1.4 million average tokens per problem. Hilbert’s comparable pass@1 result is reported with 1,880.4 million maximum tokens per problem. The paper also reports that at a fixed budget of 1 million tokens per problem, AxProverBase achieves 40% success compared with Hilbert’s 15%.

This does not mean AxProverBase is universally better than Hilbert. Benchmark comparisons are shaped by settings, budgets, model choices, datasets, and evaluation definitions. It does mean the paper raises a serious cost-performance challenge: before adding recursive decomposition, specialized fine-tuning, or elaborate tool choreography, check how far a simple verifier-centered loop can go.

That is the business-relevant punchline. The cheapest useful system is rarely the one with the fewest model calls. It is the one that gets reliable progress per unit of controlled feedback.

Minimal does not mean small, cheap, or weak

A small correction is necessary here. “Minimal” in this paper does not mean tiny.

AxProverBase is architecturally minimal, not computationally trivial. The strongest reported configuration uses Claude Opus 4.5, a 32k thinking budget, and up to 50 iterations. The cost appendix reports millions of tokens per difficult benchmark problem and an average cost of $12.6 per sample across the considered datasets, including failed proofs.

That is still efficient relative to some specialized provers, especially because the paper reports that more than 70% of the tokens are input tokens. But this is not a free lunch. It is a better-priced lunch with fewer decorative appetizers.

For business readers, the practical lesson is to separate three ideas that are often carelessly blended:

This separation matters because many AI adoption discussions still treat “simple” and “cheap” as synonyms. They are not. A simple system can be expensive. A complex system can be wasteful. The question is whether each layer earns its place.

What Cognaptus would borrow from this paper

The business pathway from AxProverBase is not “use Lean for everything.” It is also not “agents are now ready to run compliance, finance, legal, and engineering without supervision.” That would be a charming way to create expensive anecdotes.

The reusable pattern is narrower and stronger:

1. Generate an output.
2. Verify it with a deterministic, rule-based, or otherwise trusted checker.
3. Convert failure into specific diagnostic feedback.
4. Preserve the important lesson in compact memory.
5. Retry under controlled iteration limits.
6. Escalate unresolved high-level failures instead of hiding them.

This pattern applies best when a business process has clear validators. Examples include code generation against tests, financial reconciliation against accounting rules, document extraction against schema constraints, contract review against a clause library, data transformation against type and range checks, or regulatory reporting against validation rules.

The closer the process is to formal verification, the more directly the AxProverBase lesson transfers. The more ambiguous the process becomes, the more the company must invest in specification design, human review, and audit trails.

That is not a weakness of the paper. It is the whole point. Lean works because it is unforgiving. Most business environments are not unforgiving by default. They need to be made partially unforgiving through validation layers.

A practical AI operations stack inspired by this paper would look like this:

This is not glamorous. It is infrastructure. Infrastructure tends to be less glamorous than the agent demo and more likely to survive contact with accounting.

The main boundary: business validators are weaker than Lean

The strongest limitation is not that theorem proving is obscure. It is that theorem proving has a luxury many business workflows lack: a trusted formal checker.

Lean can reject invalid proof code. It can expose unsolved goals. It can identify syntax and name errors. It provides the agent with unusually clean feedback. Business workflows often have messier validators. A compliance rule may be incomplete. A contract clause may require interpretation. A customer complaint may be emotionally loaded. A financial anomaly may be valid under a rare exception.

This means companies should not copy the confidence level of theorem proving unless they also copy the verification discipline.

There are other boundaries.

First, the paper’s strongest configuration depends on a powerful frontier model. The architecture is minimal, but the model is not modest. Second, web search is included for practical usefulness, which makes the system more useful in real deployment but also means performance depends partly on external information availability. Third, the reviewer agent is an additional safety layer, not a mathematical guarantee by itself. The deterministic compiler is the core verifier; the LLM reviewer helps catch statement changes or cheating mechanisms that static checks may miss.

Finally, benchmark success does not equal business readiness. The paper directly shows that a minimal verifier-centered theorem-proving agent can be competitive across formal math benchmarks. Cognaptus infers that similar design principles can improve high-stakes business AI workflows when strong validators exist. What remains uncertain is how far this pattern transfers when validation is incomplete, subjective, or politically contested.

That boundary is not decorative caution. It determines whether the system should automate, assist, or merely prepare work for review.

The quiet lesson: better agents may look less agentic

AxProverBase is interesting because it resists the theatrical version of agent design.

There is no need to pretend the agent has a personality. No need for a committee of synthetic specialists debating in circles. No need for autonomy as a mood. The system succeeds by giving a capable model a disciplined environment: try, check, remember, search, retry.

That is a less romantic picture of AI agents, but a more useful one.

The paper’s evidence suggests that much of the practical value in agentic AI may come from moving the model into a tight feedback loop with verifiers, not from making the surrounding architecture more ornate. Iterative refinement is the largest driver. Memory is the second. Search helps, but mostly by reducing tool and library friction. Stronger models benefit more when the scaffold lets them spend less time stumbling over shallow errors and more time solving the real task.

For business leaders, the lesson is almost annoyingly pragmatic: before buying or building a grand autonomous system, define the verifier. Then define how failures become feedback. Then define what the system remembers. Only after that should search tools, model upgrades, and workflow orchestration enter the discussion.

Less can prove more. But only when “less” means disciplined design, not wishful underbuilding.

\ast\astCognaptus: Automate the Present, Incubate the Future.\ast\ast