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

We present lf-lean, a verified translation of all 1,276 statements of the Logical Foundations textbook from Rocq to Lean, produced by frontier AI with ~2 person-days of human effort versus an estimated ~2.75 person-years manually (a 350× speed-up).

Feb 5, 2026

Catching bugs with fractional proofs

We introduce fractional proof decomposition, a technique for scaling testing compute logarithmically, instead of linearly, with bug rarity. We achieve this efficiency by fusing partial evaluation and property-based testing.

Oct 7, 2025

lf-lean: The frontier of verified software engineering

Catching bugs with fractional proofs

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