Vibe Coding a Theorem Prover: When LLMs Prove (and Break) Themselves

A theorem prover is a terrible place to let an LLM improvise

Code review is forgiving compared with theorem proving.

In ordinary software, a language model can produce code that looks clean, passes a few tests, and still hides a slow-burning defect somewhere behind an edge case. Annoying, yes. Catastrophic, sometimes. But the social contract is familiar: tests catch some errors, humans catch others, production catches the rest. Very elegant. Very modern. Very expensive.

A theorem prover has a different personality. It does not care whether the proof “sounds right.” It does not admire your chain-of-thought. It does not reward confidence, fluency, or a tastefully formatted explanation. In Isabelle/HOL, a proof is accepted only if it checks against the formal system. No vibes. No partial credit. No “close enough for the demo.”

That is why Zhe Hou’s paper on Isabellm, an LLM-powered theorem prover for Isabelle/HOL, is more interesting than the usual “LLMs can reason now” headline.¹ The paper asks a neatly recursive question: can LLMs help build a theorem prover that itself uses LLMs to prove theorems? The answer is not a simple yes. It is more useful than that.

The system works when the language model is demoted.

Not removed. Not worshipped. Demoted.

Isabellm treats the LLM as a proposal engine inside a verifier-controlled machine. The model suggests proof steps. Isabelle decides whether those steps exist in reality. When that separation is clean, the system can solve some goals that defeat classical Isabelle automation such as Sledgehammer. When the separation becomes messy—especially in the higher-level proof planner and repair logic—the system starts to show exactly where today’s LLM engineering still breaks.

That makes this paper less a story about theorem proving alone and more a small case study in how serious AI systems should be designed when correctness matters.

The real architecture is proposal first, authority second

The common misconception is easy to predict: “An LLM theorem prover” sounds like an AI system that understands mathematics deeply enough to write formal proofs on its own.

That is not what Isabellm shows.

The core mechanism is more disciplined. The LLM is used as a conditional generator of possible proof commands. Each command is then executed through Isabelle. If Isabelle accepts the step, the search continues. If Isabelle rejects it, the candidate disappears. The model is not trusted; it is sampled.

This distinction matters because proof assistants already have the hard part: a trusted verifier. The bottleneck is not deciding whether a finished proof is correct. The bottleneck is finding a sequence of proof steps that the verifier will accept. Isabellm attacks that search problem.

The first layer, the stepwise prover, represents proof synthesis as bounded search over proof states. At each point, the system holds candidate proof prefixes, asks an LLM for small next actions, validates those actions with Isabelle, and keeps the best surviving states in a beam. The scoring is intentionally practical: fewer remaining subgoals are better, shorter proofs are preferred when otherwise similar, duplicate proof states are removed through fingerprints, and the search stops at depth or time limits.

This is not glamorous. That is its virtue.

A useful way to read the system is:

The business translation is already visible. In high-stakes automation, the question should not be “Can the model do the job?” It should be “Can the model propose actions inside a system that has an independent way to reject bad actions?”

That is a less exciting sentence. It is also closer to deployable engineering.

The stepwise prover works because it narrows the model’s freedom

The stepwise prover is the strongest part of the paper because it makes the LLM’s job small enough to be useful.

Instead of asking the model to generate a complete proof in one shot, Isabellm asks for short proof commands under a restricted grammar. Step mode produces intermediate commands. Finish mode produces proof-closing commands. The prompts instruct the model to output only commands, not explanations, comments, or decorative prose. The raw output is then sanitized: code fences, bullets, numbering, malformed lines, overly long commands, and duplicates are stripped away before Isabelle sees anything.

This is a familiar pattern in reliable AI systems: reduce the model’s output space before checking it.

The paper’s design turns the LLM into something closer to a stochastic search heuristic. It can suggest an induction, a simplification, a rule application, or a finishing tactic that classical automation may not try in that form. But it cannot declare victory. The proof assistant keeps the keys.

The stepwise prover also adjusts exploration. If search stagnates, the system can raise temperature to encourage more diverse candidates. If the LLM is not proposing useful actions, the prover can inject heuristic templates. If multiple paths lead to effectively the same proof state, fingerprints reduce repeated exploration. If a proof is found, the system attempts minimization: collapsing the proof, removing unused facts, deleting redundant steps, or retrying shorter one-line proofs.

This is why the paper’s reported Sledgehammer comparison is meaningful but should not be overread. The author reports that the stepwise prover can solve certain higher-order goals that Sledgehammer cannot solve even with generous timeouts. That is evidence that LLM-guided proof search can explore qualitatively different proof paths. It is not evidence that Isabellm is now a broad benchmark winner across Isabelle/HOL. The paper does not provide a large leaderboard-style result table, and pretending otherwise would be marketing with a lab coat.

The clean interpretation is narrower and stronger: LLMs can add value to formal proof search when every proposed move is cheaply and strictly checked.

That statement travels well beyond theorem proving.

Learning is useful only because the verifier produces clean feedback

Isabellm does not stop at prompting. It logs proof attempts and turns them into training data. This is one of the paper’s more business-relevant ideas because it shows how an AI workflow can improve without relying on mysterious model self-confidence.

Every attempted tactic can become a labeled example. Did Isabelle accept it? Did it reduce the number of subgoals? How long did it take? Was it a cache hit? Which premises were retrieved? Which tactic family was used? These signals feed lightweight rerankers and possible offline reinforcement learning.

The reranker is not asked to prove anything. It predicts which candidate steps are worth trying first. That is modest but operationally important. In search systems, budget matters. If a verifier call is expensive, better ordering increases the amount of useful exploration per unit of time.

Premise selection plays a similar role. Isabelle libraries can contain large numbers of available facts. Raw prompting cannot carry all of them. Isabellm therefore retrieves a small set of likely useful lemmas using TF-IDF, token overlap, or neural encoders, then exposes them as soft hints. Again, the word “soft” is doing real work. Retrieval can be wrong. The system remains robust because a retrieved premise is not accepted as relevant until it participates in a proof step that Isabelle verifies.

For business systems, this is the part worth stealing.

Many companies want AI agents that “learn from execution.” Most implementations quietly mean “store more chat history and hope the next answer is better.” Isabellm points to a more disciplined version: collect execution-grounded traces where each action has an external success signal. The verifier does not need to be Isabelle. It could be a compiler, a type checker, a policy engine, a reconciliation system, a unit-test harness, a contract validator, or a simulator with well-defined pass/fail criteria.

The general pattern is:

The principle is not “AI learns everything.” The principle is “AI learns where the validator says it was wrong.” That is much less romantic. It is also how grown-up automation survives contact with reality.

The planner is where elegance starts leaking

The second layer of Isabellm is more ambitious: a proof planner that generates structured Isar outlines, leaves explicit sorry holes, fills those holes using the stepwise prover, and then repairs failed blocks through a CEGIS-style loop.

Architecturally, the planner is attractive. It addresses a real weakness of step-by-step search: local tactics can be myopic. Longer proofs often require decomposition. A human proof engineer may introduce intermediate claims, split cases, choose an induction structure, or organize the argument into readable Isar blocks. The planner tries to automate that higher-level structure.

It samples multiple outlines at different temperatures. It normalizes raw LLM output into canonical skeletons. It extracts holes. It uses micro-RAG: lightweight symbolic hints mined from context and Isabelle corpora, including lexicon-derived associations between tokens and useful lemmas. It then fills gaps and attempts block-level repair when the script fails.

On paper, this is exactly the kind of architecture people say they want from LLM agents: plan, execute, observe failure, repair, continue.

The paper’s important contribution is showing that this is also where the system struggles.

The fill-and-repair mechanism is the weak point. The author reports that even strong LLMs used in the project struggled to implement the intended repair machinery reliably, especially once the codebase grew beyond roughly twenty files and new code had to respect existing APIs. In practice, planner repair rarely succeeds beyond trivial cases. Most successful proofs come either from the initial outline or from the stepwise prover working without much planner help.

That failure is not an embarrassing footnote. It is the most useful part of the paper.

Repairing an Isar proof is not just “fix the error message.” The system must reason about global proof structure, local proof states, context-sensitive proof modes, indentation, syntax, block boundaries, and the distinction between legal apply-style progress and a finished local proof obligation. A candidate edit may look plausible while violating a structural invariant several lines earlier. A repair target may be the visible sorry, while the real cause is an earlier have, show, case, or subproof block.

This is the classic agent problem in miniature. LLMs can often produce a plausible next action. They are much less reliable at maintaining invariants across a changing, multi-file, stateful system where every edit must preserve invisible contracts.

The paper calls the project “vibe coding” with a wink. The lesson is less cute: vibe coding can generate large amounts of machinery, but machinery with deep invariants eventually asks for engineering discipline that vibes do not provide.

The evidence is system evidence, not a leaderboard

The paper’s findings should be read according to their role.

This distinction matters because AI readers often flatten every paper into “method plus result.” Here the architecture is the result. The system demonstrates a design pattern, gives representative successes, and reports a failure boundary. It does not present a polished industrial product or a standardized benchmark victory.

That makes it more useful, not less.

A leaderboard tells you who won a controlled contest. A system paper like this tells you where the wiring burns.

The business value is validator-gated automation, not autonomous proof magic

For business readers, formal theorem proving may sound remote. Most firms are not writing Isabelle proofs on Monday morning. They are trying to automate compliance review, financial controls, software QA, contract analysis, risk workflows, and internal decision processes where errors are expensive and explanations are audited after the damage is done.

The Isabellm lesson applies because those domains share a structure: the model can propose, but something stricter must dispose.

What the paper directly shows is limited. It shows an Isabelle/HOL system where LLMs, beam search, premise hints, reranking, and verifier feedback can produce useful proof search behavior on a laptop-scale setup. It also shows that higher-level repair remains unreliable.

What Cognaptus infers is broader: businesses should design AI automation around executable gates wherever possible. The LLM should not be the final judge in workflows with legal, financial, safety, or infrastructure consequences. It should generate candidate actions, explanations, mappings, or scripts that are checked by systems with clearer semantics.

That changes the ROI conversation.

The near-term value is not eliminating experts. It is reducing the amount of low-level search experts must perform. A proof engineer may still define the right lemma. A compliance officer may still decide the policy interpretation. A senior developer may still own the architecture. But AI can search through candidate steps, draft structured possibilities, retrieve related facts, and surface validated partial progress.

This is cheaper diagnosis, not magical replacement.

The strongest business pattern is:

1. Constrain the action space. Do not let the model emit arbitrary prose when the next system expects a typed action, rule, command, or patch.
2. Validate every consequential action. The authority should be a checker, engine, simulator, or human-controlled review process—not the model’s tone.
3. Log failures as assets. A rejected action is not waste if it becomes training data for future prioritization.
4. Separate local execution from global planning. The model may be good at local moves while still unreliable at maintaining system-wide invariants.
5. Treat repair as its own product problem. “The agent will fix itself” is not a design. It is a future incident report.

The mildly sarcastic version: if your AI system has no independent validator, you have not built an agent. You have built a confident intern with API access.

The boundary is planning under invariants

The most important limitation is not that Isabellm fails sometimes. Every proof system fails often; theorem proving is hard. The important limitation is where it fails.

The stepwise prover’s world is narrow. It proposes one command, gets feedback, updates the state, and tries again. This is a good environment for LLM assistance because the feedback loop is short and the validator is decisive.

The planner’s world is wider. It must preserve structure across multiple proof blocks, holes, repairs, regenerated subproofs, and local contexts. A repair can be syntactically plausible but semantically misplaced. A block can be locally reasonable but globally incompatible. A model can respond to an error message while quietly violating an API or proof-mode assumption elsewhere.

That is why the paper’s repair failure should not be dismissed as merely an implementation issue. It points to a general difficulty in LLM systems: models are often strongest when the environment can quickly reject a local action, and weakest when success depends on maintaining a web of latent constraints over time.

This boundary matters for enterprise automation. Many business workflows look like planners, not stepwise provers. They involve exceptions, policy hierarchy, cross-document dependencies, changing states, hidden assumptions, and partial repairs. An LLM can draft a solution. It may even draft five. But unless the environment can check the invariants, the system is only performing competence.

The practical conclusion is not “avoid LLM planners.” It is “do not confuse planner-shaped output with planner-grade reliability.”

Why this paper matters beyond Isabelle

The most durable idea in the paper is architectural humility.

Isabellm does not ask the LLM to become a formal authority. It asks the LLM to be useful inside a formal authority. That is the right direction for many AI systems. It replaces the fantasy of autonomous intelligence with a more realistic division of labor:

• models generate candidates;
• symbolic systems check candidates;
• search procedures allocate budget;
• logs turn execution into training data;
• humans decide where the specification comes from.

There is a quiet lesson here for AI product builders. The most valuable AI systems may not be the ones that sound most human. They may be the ones whose mistakes are easiest to reject, record, and learn from.

Isabellm is therefore not just a theorem prover story. It is a warning about where “vibe coding” stops. LLMs can help build complex systems and operate inside them, but the moment the task requires maintaining strict global invariants across a growing codebase, the old engineering virtues return: interfaces, tests, logs, modularity, verification, and boring discipline.

The paper’s title invites a joke. The system’s design delivers the serious version.

Vibes can propose. Verifiers must decide.

Cognaptus: Automate the Present, Incubate the Future.