用大模型自动证明Isabelle定理，可在普通电脑运行。
Vibe Coding an LLM-powered Theorem Prover
- 结合大模型与Isabelle验证，分步生成并修复证明
- 能解决传统工具无法处理的复杂定理，如Sledgehammer失败的命题
- 适合对自动化证明感兴趣的研究者和开发者
我们提出Isabellm，一个基于大语言模型的Isabelle/HOL全自动定理证明系统。该系统可在本地LLM（如Ollama）或Gemini CLI等API上运行，适配消费级计算机。其框架包含分步证明器（使用大模型提出命令，通过Isabelle有限搜索验证）与高层证明规划器（生成结构化Isar大纲并填充/修复残缺部分）。集成技术包括：策略束搜索、策略重排序的机器学习与强化学习模型、小型Transformer用于前提选择、基于AFP的微RAG用于Isar证明，以及反例引导的证明修复。所有代码由GPT 4.1–5.2、Gemini 3 Pro、Claude 4.5实现。实验表明，Isabellm可证明某些连Isabelle标准自动化（如Sledgehammer）也无法解决的引理，展现其实际价值。但我们也发现，即使最先进的模型如GPT 5.2 Extended Thinking和Gemini 3 Pro，在实现复杂算法设计的填充修复机制时仍不可靠，凸显大模型代码生成与推理的根本挑战。代码已开源：https://github.com/zhehou/llm-isabelle。
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。