Wrap large language models with proof assistants (e.g., Lean4) so model‑proposed reasoning steps are autoformalized and mechanically proved before being accepted. Verified steps become a retrievable database of grounded facts, and failed proofs feed back to the model for revision, creating an iterative loop between probabilistic generation and symbolic certainty.
— If deployed, this approach could change how we trust AI in math, formal sciences, safety‑critical design, and regulatory submissions by converting fuzzy model claims into machine‑checked propositions.
Steve Hsu
2026.09.12
90% relevant
The article documents the exact feedback loop the existing idea describes: Large language models emit Lean‑checked proofs (DeepMind’s AlphaProof, Mathlib growth), and that formal corpus then trains better automated provers. It adds a concrete qualification: Lean’s kernel mechanically verifies derivations from axioms but cannot certify that formal definitions (e.g., the construction of the real numbers `ℝ`) capture the mathematician’s intended continuum—so the article refines the existing idea by highlighting a semantic gap that matters as verification becomes automated and scaled.
Alexander Kruel
2025.12.01
100% relevant
Hermes architecture described in the post: LLM → autoformalizer → Lean4 prover → memory of proved steps (arXiv:2511.18760v1).
← Back to all ideas