I built FuturLang, a formal verification system that preserves natural language structure while enabling machine verification. The goal is to make formal proofs more accessible without requiring specialized notation like Coq/Lean/Agda. Example proof structure:

(1) It is assumed that: (√2 is rational) (2) This implies that: (∃ integers a, b)... (3) Therefore: (√2 is irrational)

I’ve built the language spec, verification engine, and a database of 250+ proofs. But adoption has been minimal, which makes me question if this addresses a real need. Questions for HN: ∙ Is “natural language + formal verification” solving a real problem? ∙ What would need to be true for you to use this instead of Lean/Coq? ∙ Am I building a solution in search of a problem? Honest feedback welcome - trying to decide whether to keep building or move on. GitHub: https://github.com/wenitte/mathematical-intelligence