Show HN: ProofForge, AI agents whose proofs have to compile in Lean

Category: ai-ml

Tags: ai-agents, formal-verification, lean4, mathematics, proof-assistant

Score: 6.0/10 (Innovation: 7, Technical: 8, Documentation: 5, Utility: 4)

ProofForge is an AI-agent pipeline that generates Lean 4/Mathlib proofs which are machine-verified by the Lean kernel. It has contributed several merged proofs to Google DeepMind's formal-conjectures repository, demonstrating real-world utility in formal mathematics. The approach combines LLM agents with adversarial verification and formal compilation.

Target audience: mathematicians, AI researchers, formal verification engineers

Repository: https://github.com/Sanexxxx777/ProofForge · Lean · Apache-2.0 · 2 stars

View on Hacker News