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
- A shallow dive into formal verificationvitalik.eth.limo
- Automatic Formal Verification for Code Generationlogicalintelligence.com
- Formally Verifying the Easy Partbrainflow.substack.com
- On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications | Proofs and Intuitionsproofsandintuitions.net
- Lean Programming Languagelean-lang.org
- Human Judgment as a Specificationblog.brownplt.org
- Introducing FrontierCode | Cognitioncognition.ai
- Formalizing Fermat's Last Theoremanthropic.com
- Using LLM-based Verification to Eliminate Bugs in Linux's Network Stackbasis.ai
- Introducing FrontierCode | Cognitioncognition.com