lf-lean: The frontier of verified software engineering | Theorem
theorem.dev · 5,884 words · saved by 1 readers
lf-lean is a verified translation from Rocq to Lean of all 1,276 statements in Logical Foundations, done by frontier AI 350× faster than humans.
Introduction As AIs automate increasingly complex software tasks, a fundamental tension emerges: how do we know the code they produce is correct? The standard approach of reviewing AI-generated code and its tests doesn't scale. Human review effort grows proportionally with code volume, while AI code generation capacity grows exponentially. 1 1 Moreover, frontier software engineering typically results in multiplicative bug growth; many bugs are subtle and interaction-driven, and their count grows super-linearly with code length and complexity. See Appendix C . If this trend continues, we're hea
saved by
related reading
- When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
- Lean Software Scaling Laws · Gwern.netgwern.net
- FLT: Anthropic has beaten me to itxenaproject.wordpress.com
- Asymmetry of verification and verifier’s rule - Jason Weijasonwei.net
- Lean (proof assistant) - Wikipediaen.wikipedia.org
- Lean Programming Languagelean-lang.org
- Dear Agent: Prove it. • Rijnard van Tonderrijnard.com
- Formally Verifying the Easy Partbrainflow.substack.com
- Automatic Formal Verification for Code Generationlogicalintelligence.com
- Your job is to deliver code you have proven to worksimonwillison.net
- Formalizing Fermat's Last Theoremanthropic.com
- AI Will Write All the Code. Mathematics Will Prove It Works.menlovc.com