The large language models (LLMs) might produce a persuasive argument within mathematical and logical fields, although such argument often includes some minor missteps, including the entire omission of side conditions, invalid inference patterns, or appeals to a lemma that cannot be derived logically out of the context being discussed. These omissions are infamously hard to notice solely out of the text, as even the misconstrued construction still may seem mostly accurate. Conversely, interactive theorem provers like Lean and Coq have rigorous reliability by ensuring that syntactic and semantic statements only accept statements that can pass all the syntactic and semantic steps in the program which is a small trusted kernel of the language type-checks with. Despite the fact that this technique provides strong guarantees, it comes at quite a heavy price: the evidence must be completely formalized, and the evidence user or a auxiliary search program must provide an avalanche of low-level information. This paper presents a hybrid pipeline where an LLM generates a typed proof sketch in a compact DSL and a lightweight trusted kernel expands the sketch into explicit proof obligations.
Figures & tables
Fig. 1: ProofSketcher architecture: LLM proposes a typed sketch; a lightweight trusted kernel extracts obligations; external solvers are untrusted and must provide certificates checked by a trusted checker; failures yield structured feedback for local repair; caching enables incremental re-checking.
Method
miniF2F-test (Pass %)
LeanDojo-test (Pass %)
ProofNet-test (Pass %)
ReProver (LeanDojo) [ 28 ]
26.64%
51.20%
13.98%
DeepSeek-Prover [ 26 ]
50.00%
–
–
DeepSeek-Prover-V2 [ 27 ]
88.93%
–
37.10%
ProofSketcher (Ours)
92.21%
58.25%
44.62%
TABLE I: Kernel-Accepted Pass Rate (%) on Formal Reasoning Benchmarks
Fig. 2: Pass rate by benchmark and method.
Fig. 3: Mean LLM calls per theorem (lower is better).
Fig. 4: Mean time per theorem: kernel vs solver time.
We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design choices are a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file. Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark. Lean output excerpts: https://github.com/xiyuzhai-husky-lang/visored/
Xiyu Zhai, Xinyi Chen, Yiping Wang +3
University of Washington · University of Innsbruck
LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study (n=16) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.
Hita Kambhamettu, Will Crichton, Sean Welleck +2
University of Pennsylvania Philadelphia, PA, USA · Brown University Providence, RI, USA · Carnegie Mellon University Pittsburgh, PA, USA +1
Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@k and refine@k metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of <\0.01$ per correct proof.
Tyson Klingner, Drew Bladek, Escher Crawford +6
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA