Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Vibe Coding an LLM-powered Theorem Prover

Zhe Hou

TL;DR

Isabellm addresses the challenge of fully automatic proving in Isabelle/HOL by integrating an LLM-guided stepwise prover with a high-level Isar proof planner, operating in a verifier-in-the-loop on consumer hardware. The system treats proof synthesis as bounded search using a beam of candidate states and leverages LLMs to propose local commands that are validated by Isabelle, supplemented by premise retrieval and a learning-based reranker to manage search complexity. A higher-level planner uses diversified Isar skeleton outlines, Micro-RAG hints, and a structured fill/repair loop (CEGIS-style) to close gaps, though the authors report substantial limitations in current LLM capabilities for reliable repair at scale. The work provides a data-generating, reproducible framework with run- and attempt-level logging to enable continual learning and evaluation, and demonstrates practical benefits by solving lemmas beyond Sledgehammer in some cases while highlighting core challenges in scalable, automatic proof repair. Overall, Isabellm represents a concrete step toward laptop-friendly, automatic theorem proving that combines learning signals with formal verifier guarantees, while outlining clear directions for improving planning and repair in future work.

Abstract

We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemini CLI, and it is designed to run on consumer grade computers. The system combines a stepwise prover, which uses large language models to propose proof commands validated by Isabelle in a bounded search loop, with a higher-level proof planner that generates structured Isar outlines and attempts to fill and repair remaining gaps. The framework includes beam search for tactics, tactics reranker ML and RL models, premise selection with small transformer models, micro-RAG for Isar proofs built from AFP, and counter-example guided proof repair. All the code is implemented by GPT 4.1 - 5.2, Gemini 3 Pro, and Claude 4.5. Empirically, Isabellm can prove certain lemmas that defeat Isabelle's standard automation, including Sledgehammer, demonstrating the practical value of LLM-guided proof search. At the same time, we find that even state-of-the-art LLMs, such as GPT 5.2 Extended Thinking and Gemini 3 Pro struggle to reliably implement the intended fill-and-repair mechanisms with complex algorithmic designs, highlighting fundamental challenges in LLM code generation and reasoning. The code of Isabellm is available at https://github.com/zhehou/llm-isabelle

Vibe Coding an LLM-powered Theorem Prover

TL;DR

Isabellm addresses the challenge of fully automatic proving in Isabelle/HOL by integrating an LLM-guided stepwise prover with a high-level Isar proof planner, operating in a verifier-in-the-loop on consumer hardware. The system treats proof synthesis as bounded search using a beam of candidate states and leverages LLMs to propose local commands that are validated by Isabelle, supplemented by premise retrieval and a learning-based reranker to manage search complexity. A higher-level planner uses diversified Isar skeleton outlines, Micro-RAG hints, and a structured fill/repair loop (CEGIS-style) to close gaps, though the authors report substantial limitations in current LLM capabilities for reliable repair at scale. The work provides a data-generating, reproducible framework with run- and attempt-level logging to enable continual learning and evaluation, and demonstrates practical benefits by solving lemmas beyond Sledgehammer in some cases while highlighting core challenges in scalable, automatic proof repair. Overall, Isabellm represents a concrete step toward laptop-friendly, automatic theorem proving that combines learning signals with formal verifier guarantees, while outlining clear directions for improving planning and repair in future work.

Abstract

We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemini CLI, and it is designed to run on consumer grade computers. The system combines a stepwise prover, which uses large language models to propose proof commands validated by Isabelle in a bounded search loop, with a higher-level proof planner that generates structured Isar outlines and attempts to fill and repair remaining gaps. The framework includes beam search for tactics, tactics reranker ML and RL models, premise selection with small transformer models, micro-RAG for Isar proofs built from AFP, and counter-example guided proof repair. All the code is implemented by GPT 4.1 - 5.2, Gemini 3 Pro, and Claude 4.5. Empirically, Isabellm can prove certain lemmas that defeat Isabelle's standard automation, including Sledgehammer, demonstrating the practical value of LLM-guided proof search. At the same time, we find that even state-of-the-art LLMs, such as GPT 5.2 Extended Thinking and Gemini 3 Pro struggle to reliably implement the intended fill-and-repair mechanisms with complex algorithmic designs, highlighting fundamental challenges in LLM code generation and reasoning. The code of Isabellm is available at https://github.com/zhehou/llm-isabelle
Paper Structure (79 sections, 49 equations, 2 figures)

This paper contains 79 sections, 49 equations, 2 figures.

Table of Contents

  1. Introduction
  2. An LLM-powered Stepwise Prover
  3. Preparation
  4. Candidate generation via language models
  5. Invocation model.
  6. Prompting modes.
  7. System prompts.
  8. User prompt construction.
  9. Decoding control and exploration.
  10. Candidate sampling.
  11. Post-processing and sanitisation.
  12. Integration with reranking.
  13. Heuristic variant injection.
  14. Design rationale.
  15. Beam expansion and scoring
  16. ...and 64 more sections

Figures (2)

  • Figure 1: An illustration of the integration with Isabelle/jEdit.
  • Figure 2: An example of a proof inserted by the LLM prover.