HackTalk: Jason Gross (Theorem)
HackTalk: Jason Gross (Theorem)
Pre-hackathon talk for the Secure Program Synthesis Hackathon, May 22-24 online. Free and open. Recording available after.
Theorem's pitch is straightforward: build AI that is as capable at program verification as it is at writing Python. Recent work includes lf-lean, an AI system that translated 1,276 logical-foundations statements from Rocq to Lean 350x faster than humans, and fractional proofs, a technique blending partial evaluation with property-based testing.
Jason Gross is the Co-founder of Theorem, an AI and programming languages research lab. Theorem is YC Spring 2025, backed by a $6M seed from Khosla Ventures. Jason holds a PhD from MIT, where he developed Fiat Cryptography, the verified code generator that produces the cryptographic primitives running inside trillions of HTTPS connections daily. He reported the plurality of all-time bugs in the Rocq proof assistant and joined its dev team to help fix them.
Topics: how Theorem fits verification into the AI coding loop, what lf-lean and fractional proofs change about the cost curve, and where this maps onto the four hackathon tracks (spec elicitation, spec validation, spec-driven development, adversarial robustness).
Format: 15-25 min talk + ~15 min Q&A. Zoom, livestreamed and recorded.
Co-organized by Apart Research and Atlas Computing.