Theorem

Theorem is building AI that is as capable at program verification as it is at writing Python.

Research

`lf-lean`: The frontier of verified software engineering

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.

Feb 5, 2026

Catching bugs with fractional proofs

Fractional proof decomposition fuses partial evaluation and property-based testing to scale testing compute logarithmically with bug rarity, instead of linearly.

Oct 7, 2025

lf-lean: The frontier of verified software engineering

Catching bugs with fractional proofs

`lf-lean`: The frontier of verified software engineering