Zero Knowledge · Zero Knowledge Podcast

Kevin Lacker on AI-Assisted Theorem Proving and Acorn

October 22, 2025·56 min·4 clips

Kevin Lacker explains how his theorem prover Acorn uses AI to check mathematical proofs in real-time.

1. Zero Knowledge hosts Anna Rose and Guillermo speak with Kevin Lacker, creator of the Acorn Theorem Prover, about AI-assisted formal mathematics. 2. Kevin's background spans software engineering at Google and Facebook, founding two Y Combinator companies including Parse (a mobile developer database tool), and competing in the International Math Olympiad and Putnam exam. 3. The episode's core thesis: can an integrated AI model eliminate the verbosity of existing theorem provers like Lean and make formal mathematics accessible to working mathematicians? 4. Guillermo frames why existing formal provers 'suck in every fucking possible way': systems like Lean require users to explicitly justify every trivial step, including commutativity of addition (named 'add_com'), which no mathematician would state out loud. 5. Kevin explains that Acorn differs from Lean by removing the separate 'tactics' language — users write mathematical statements and the AI fills in the justification steps, similar to explaining a proof to a smart friend rather than to a pedantic computer. 6. Acorn runs as a VS Code extension: each time the user saves a line, the embedded local AI model checks it and returns either a checkmark (proved), yellow squiggle (needs more steps), or red squiggle (syntax error). 7. Kevin walks through a live example — proving that an odd number plus one is even — showing how a few lines of near-natural-language Acorn code replace dozens of tactic invocations in Lean. 8. Kevin describes selecting the entry point for Acorn's design by asking: if an AI could solve all the awkward parts automatically, what would the ideal human interface look like? The answer was something closer to Python than to Rust or C++. 9. The embedded AI model is trained on AcornLib, Acorn's own mathematical library, and is small enough to run locally so feedback is near-instantaneous during proof writing. 10. Guillermo introduces the flywheel: every new theorem added to AcornLib trains the AI on the techniques used, which lowers the cost of proving subsequent theorems, creating a compounding improvement cycle. 11. Kevin compares AcornLib to Lean's MathLib — an attempt to encode all known mathematics as verified statements — but notes that Acorn's AI integration makes contributions easier and enables the library to self-reinforce. 12. Kevin estimates that once the AI can parse math PDFs, the system could ingest the roughly 100 new math papers published per day, eventually building a queryable index of all known mathematical knowledge. 13. Guillermo raises a live disagreement: he argues that Qwen 4B Thinking, a 4-billion-parameter model small enough to run on a phone, already produces complete convincing proofs for non-trivial convex optimization problems without being a well-known training example. 14. Kevin acknowledges the risk of claiming anything is impossible in AI, noting that 'there's a million people on a hundred billion dollars trying to prove you wrong,' and that the local model ceiling is still unknown. 15. The conversation touches on Principia Mathematica by Russell and Whitehead — described as an enormous early-20th-century attempt to derive all mathematics from axioms, reaching 'two plus two equals four' only by page 200. 16. Kevin describes Acorn's axiomatic base: inductive structures (lists and natural numbers), substitution rules, and equality rules form a small fixed set from which integers, rationals, reals, and sets are derived. 17. The episode's tone is a three-way technical conversation, with Guillermo acting as a knowledgeable co-host who regularly challenges Kevin and adds independent perspectives from his own blog post on the topic. 18. Anna plays the generalist role, asking clarifying questions that ground abstract concepts — comparing Acorn's real-time feedback to Rust's borrow checker, and probing whether Acorn is a language, a toolset, or a product. 19. Mathematicians, CS researchers, and software engineers curious about how AI is changing formal proof systems will find the most value here. 20. Listeners with no interest in programming languages, formal logic, or the technical infrastructure of mathematics will likely not engage with this episode.

As heard by us

A grounded look at AI helping prove things without pretending the hard parts went away.

Kevin Lacker's Acorn story treats theorem proving as a practical workflow, not a magic trick. The useful part is the tension between what software can check, what AI can automate, and where a person still has to draw the line.

Read the full review in PlayNext →

Why you'd press play

Want AI that checks proofs instead of just chatting about them?

Read the full recommendation in PlayNext →

Listen to the show on

Apple Podcasts Spotify

Play clips from this episode More from Zero Knowledge