Show HN: FuturLang – Natural language formal verification

1 pointsby wapiou5개월 전1 comments

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

1 comments

ndgold5개월 전

I think formal verification is super valuable use case and would love to learn more about how to experiment with it through this tool, which may not have the immediate traction it needs to grow but I dig it and want to learn more