TLDR: HILBERT is an agentic AI framework that significantly improves automated theorem proving by integrating the informal mathematical reasoning of large language models (LLMs) with the precise verification of formal systems like Lean 4. It achieves this through recursive problem decomposition, leveraging a reasoner LLM, a prover LLM, a formal verifier, and a semantic theorem retriever, leading to state-of-the-art performance on challenging mathematical benchmarks like miniF2F and PutnamBench.
A groundbreaking new AI framework named HILBERT is making significant strides in the field of automated mathematical theorem proving. Developed by researchers from UC San Diego and Apple, HILBERT aims to bridge the performance gap between the impressive, yet often error-prone, informal reasoning abilities of large language models (LLMs) and the absolute accuracy of formal theorem proving systems like Lean 4.
While general-purpose LLMs have shown remarkable capabilities in solving complex mathematical problems, their solutions frequently contain subtle errors that are difficult to detect. Formal systems, on the other hand, guarantee correctness but have historically struggled to solve as many problems as their natural language counterparts. HILBERT tackles this challenge by combining the best of both worlds.
How HILBERT Works: A Multi-Agent Approach
HILBERT operates as an agentic framework, orchestrating four key components to construct and verify mathematical proofs:
- Reasoner: A general-purpose LLM (like Google Gemini 2.5 Pro/Flash) that excels at informal mathematical reasoning, generating proof sketches and interpreting errors.
- Prover: A specialized LLM (such as DeepSeek-Prover-V2-7B or Goedel-Prover-V2-32B) optimized for generating formal Lean 4 tactics.
- Verifier: A formal language verifier (Kimina Lean Server) that automatically checks the correctness of theorem statements and proofs with complete accuracy.
- Retriever: A semantic search engine that fetches relevant theorems and definitions from Mathlib, a vast library of formalized mathematics.
The process begins with HILBERT attempting a direct proof using the Prover. If this fails, it employs a recursive decomposition strategy. The Reasoner breaks down the complex problem into smaller, more manageable subgoals. For each subgoal, HILBERT first tries to solve it with the Prover. If that doesn’t work, it falls back to a “shallow solve” approach using the Reasoner, augmented with retrieved theorems. If subgoals still remain unproven, the system recursively decomposes them further until they are resolved. Crucially, HILBERT leverages feedback from the Verifier at every stage to identify and correct errors, guiding the refinement of proofs as needed.
Also Read:
- PRISM: A Dynamic Strategy Framework for Enhanced Mathematical Reasoning in LLMs
- DeepSearch: Enhancing Language Model Reasoning Through Integrated Tree Search Training
Achieving State-of-the-Art Performance
HILBERT has demonstrated exceptional performance on challenging mathematical benchmarks:
- miniF2F: It achieved an impressive 99.2% pass rate, surpassing the best publicly available method by 6.6 percentage points.
- PutnamBench: On this highly challenging dataset of undergraduate-level problems, HILBERT solved 462 out of 660 problems (70.0% pass rate). This significantly outperforms proprietary approaches like SeedProver (50.4%) and represents a 422% improvement over the best publicly available baseline.
The research highlights that the choice of the informal reasoner LLM is particularly critical, with Gemini 2.5 Pro consistently yielding better results than its Flash variant. Ablation studies further confirmed the effectiveness of HILBERT’s core innovations: the recursive decomposition procedure for breaking down complex proofs and the retrieval-augmented generation mechanism for enhancing reasoning capabilities and computational efficiency.
By systematically combining the intuitive power of informal reasoning with the undeniable rigor of formal verification, HILBERT effectively narrows the gap between these two paradigms in automated theorem proving. The framework’s ability to generate extensive proofs, sometimes exceeding 15,000 lines of code, showcases its capacity to tackle problems far beyond the reach of traditional LLMs. The full research paper can be found here.
The developers envision HILBERT as a foundation for training even more capable AI models in the future, creating a virtuous cycle where generated proofs and reasoning traces can be used to continuously advance formal reasoning abilities.
