Week 12 Lecture 1: Machine-Assisted Proofs
Due to travel, there is no in-class meeting for this lecture. These notes are therefore intended to be read outside of class.
In the first lecture, I mentioned that we use the word computer-assisted proof in a very specific meaning in this course:
A computer-assisted proof is a proof for which the verification of the proof requires so many computations that it is unfeasible to verify by hand.
This excludes cases where a computer is used in the generation of the proof, but not in the verification. In particular, it excludes proofs generated using generative AI (unless, of course, the generated proof requires a computer to verify).
Many authors have a wider definition of what it means for a proof to be computer-assisted. In particular, this includes Terence Tao, though he primarily uses the term Machine-assisted proof. This includes everything from rigorous numerics and Lean to generative AI. He gave a talk about machine-assisted proofs at the Simons Foundation in February 2025. You can watch his lecture.