lf-lean

lf-lean is a research benchmark by Theorem in which frontier AI models and Theorem’s verification stack translate all 1,276 theorems and definitions from the Logical Foundations volume of Software Foundations from Rocq to Lean, then mechanically prove each Lean translation equivalent to the original, reducing an estimated 2.7–2.75 person‑years of verification effort to about two person‑days and illustrating roughly 350× speed-ups in verified software engineering workflows.

Endorsements support Theorem Labs.

No endorsements yet.

Discussion

Start Date

-

End Date

-

Expected Duration

-

Funding Raised to Date

-