**Show HN: ProofForge, AI agents whose proofs have to compile in Lean** > AI-ag

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

> AI-agent pipeline producing machine-verified Lean 4 proofs — four PRs merged into Google DeepMind's formal-conjectures - Sanexxxx777/ProofForge ProofForge An AI-agent pipeline that produces machine-verified Lean 4 / Mathlib proofs. Agents decompose a problem, prove the pieces, and formalize them in Lean. The Lean kernel rechecks every step: \#print axioms shows only the standard axioms, and native\_decide is never used...

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-09-27 04:44（北京时间）
- **原文**：[打开原文](https://github.com/Sanexxxx777/ProofForge)