AI RESEARCH
Hilbert: Recursively Building Formal Proofs with Informal Reasoning
arXiv CS.AI
•
ArXi:2509.22819v2 Announce Type: replace Large Language Models (LLMs) nstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically checked. Formal theorem proving systems such as Lean 4 offer automated verification with complete accuracy, motivating recent efforts to build specialized prover LLMs that generate verifiable proofs in formal languages. However, a significant gap remains: current prover LLMs solve substantially fewer problems than general-purpose LLMs operating in natural language. We