Kevin Lacker on AI-Assisted Theorem Proving and Acorn
Zero Knowledge
00:00
Accepting imperfect proofs and long-term cleanliness
Guillermo and Kevin debate accepting AI-generated but messy proofs and later cleaning them while keeping correctness guaranteed.
Play episode from 35:21
Transcript
