rademaker

In his latest essay, Leonardo de Moura makes a compelling case that if AI is going to write a significant portion of the world’s software, then verification must scale alongside generation. Testing and code review were never sufficient guarantees, even for human-written systems; with AI accelerating output, they become fundamentally inadequate. Leo argues that the only sustainable path forward is machine-checked formal verification — shifting effort from debugging to precise specification, and from informal reasoning to mathematical proof checked by a small, auditable kernel. This is precisely the vision behind Lean: a platform where programs and proofs coexist, enabling AI not just to generate code, but to generate code with correctness guarantees. Rather than slowing development, Lean-style verification enables trustworthy automation at scale.

I have been working on that direction with Lean Theorem Prover (https://leanprover.github.io). There is also works using Coq (https://link.springer.com/chapter/10.1007/978-3-642-35786-2_...)

That is SUMO Ontology (http://ontologyportal.org)! It is open, in GitHub and people can contribute.

In my machine it took seconds.