technologyOct 22, 202555:43pending
Kevin Lacker on AI-Assisted Theorem Proving and Acorn
About this episode
In this episode, Anna Rose and Guillermo Angeris talk with Kevin Lacker, creator of Acorn, a theorem prover utilising AI. They explore what theorem provers are, their history, and how they're used today. Kevin shares how Acorn brings in AI to simplify the proving process, letting users naturally write mathematical statements while the system checks the correctness of those statements. It's built to feel more like natural math, unlike tools like Lean that demand every step.
They also explore the benefits of including AI in math, and also the challenges that come with it such as hallucinations, and how Acorn could speed up research in areas like zero-knowledge proofs. The dicussion also covers the history of mathematics, community building around Acorn and its open math library, acornlib.
Related Links
ZK Whiteboard Sessions is an educational video series produced by ZK Hack. It is focused on the building blocks of zero knowledge technology. Find season 3 of the Whiteboard Sessions as well as previous seasons here.
Check out the latest jobs in ZK at the ZK Podcast Jobs Board.
**If you like what we do:** * Find all our links here! @ZeroKnowledge | Linktree * Subscribe to our podcast newsletter * Follow us on Twitter @zeroknowledgefm * Join us on Telegram * Catch us on YouTube **Support the show:** * Patreon * ETH - Donation address * BTC - Donation address * SOL - Donation address * ZEC - Donation address Read transcript
- Guillermo’s Blog Post:Acorn and the future of (AI?) theorem proving
- Acorn Theorem Prover
- Acorn Standard Library:acornlib
- Lean Theorem Prover
ZK Whiteboard Sessions is an educational video series produced by ZK Hack. It is focused on the building blocks of zero knowledge technology. Find season 3 of the Whiteboard Sessions as well as previous seasons here.
Check out the latest jobs in ZK at the ZK Podcast Jobs Board.
**If you like what we do:** * Find all our links here! @ZeroKnowledge | Linktree * Subscribe to our podcast newsletter * Follow us on Twitter @zeroknowledgefm * Join us on Telegram * Catch us on YouTube **Support the show:** * Patreon * ETH - Donation address * BTC - Donation address * SOL - Donation address * ZEC - Donation address Read transcript
Get every episode summarized
Each time Zero Knowledge publishes, we email you a written briefing from the transcript — the topics, who appeared, and any specific claims, with the ad reads skipped.
Email me new episodesFree for 3 shows. No card needed.
No transcript yet
This episode has not been transcribed. Request it and it moves to the front of the queue.
More episodes
More from Zero Knowledge
The Evolution from ZKP2P to Peer with Richard Liang
Zero Knowledge
Sep 9, 202646:00completed
Minimmit, Multimmit and the New Consensus Frontier with Patrick O'Grady
Zero Knowledge
Aug 5, 20261:12:01pending
Private Information Retrieval (PIR) with Alex Hoover
Zero Knowledge
Jul 29, 20261:04:13pending
Alex Ozdemir on where Theorem Provers and ZK meet
Zero Knowledge
Jul 15, 20261:01:57pending