Vibe Coding an LLM-powered Theorem Prover

TL;DR

Isabellm is an LLM-powered theorem prover for Isabelle/HOL that automates proof synthesis using large language models, combining stepwise proof commands, structured proof planning, and various ML techniques, demonstrating both capabilities and limitations of current LLMs in formal reasoning.

Contribution

This work introduces Isabellm, a novel LLM-based framework for fully automatic theorem proving in Isabelle/HOL, integrating multiple ML components and proof strategies.

Findings

Can prove lemmas beyond Isabelle's standard automation

State-of-the-art LLMs struggle with complex proof repair mechanisms

Highlights challenges in LLM code generation for formal reasoning

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