Naproche: a proof assistant that reads math proofs written in controlled natural language
zetalyrae · x · 2026-09-23
zetalyrae highlights Naproche, a proof assistant that takes input in a controlled natural language, somewhat like Inform7. It's not just a proof checker: Naproche translates natural-language proofs into a formula representation, generates proof obligations for each step, and uses automated theorem provers to verify them. The language is embedded in LaTeX, letting mathematicians mix natural argumentative prose with symbols; the post shows a Cantor theorem proof written this way. Students have formalized various undergraduate mathematics in it, and a EuroProofNet school on natural formal mathematics runs in Bonn, June 3–5, 2025.
Related event: Naproche: A Proof Assistant for Controlled Natural Language Math(2 posts)→
More from Research
- Microsoft's Taste-Bench: best frontier model scores only 59.7% on long-horizon agent decisions — microsoft · 2026-09-23
- StableVQ: three lightweight fixes for stable vector-quantized tokenizer training — Kwai-Kolors · 2026-09-23
- Lean Pool: an AI-agent-maintained archive of formalized mathematics — Vasily Ilin · 2026-09-23
- Steering-vector loom: turning n completions into vectors to steer model output — repligate · 2026-09-23
- The 1982 Hopfield network is mathematically equivalent to transformer attention — seanmcdonaldxyz · 2026-09-23
- Schmidhuber's annotated AI history: from 1676 chain rule to modern deep learning — SchmidhuberAI · 2026-09-23