Isabellm: A playground for Free and Lightweight LLM-Guided Isabelle/HOL Provers
A research playground that guides an Isabelle/HOL theorem prover with large language models, combining LLM-proposed tactics with Isabelle's own nitpick, quickcheck, and sledgehammer, and a beam search over proof outlines.
llm-isabelle implements an Isabelle/HOL theorem prover guided by large language models accessed through Ollama, the Gemini CLI, and other backends. A stepwise prover has the LLM guess tactics, combines them with Isabelle's nitpick, quickcheck, and sledgehammer, reranks candidates with a trained model, and selects relevant premises using encoders and transformers, searching with beam search.
A separate Isar-style proof outline generator proposes a beam of structured outlines with an LLM and fills the earliest hole in the exact Isabelle proof context, preserving local theory declarations, with staged local, subproof, and whole-proof repair, a small retrieval-augmented corpus extracted from the Archive of Formal Proofs, and an experimental CEGIS-style iterative repair mode.
It requires Python 3.10-3.12 and a working Isabelle/HOL installation (tested against Isabelle2025), and is associated with the paper "Vibe Coding an LLM-powered Theorem Prover."