Interactive theorem proving demo: infinitely many primes
Channel: Scott Morrison
Date: 2020-02-20

This is a little demo of what it's like to use an interactive theorem prover, in particular Lean.

(Warning --- the automation in this demo is cheating; it's been tweaked for this particular problem, and more powerful than what we really have available right now!)

This is a segment out of a longer talk at the UC Berkeley mathematics colloquium. https://youtu.be/SfLN34hgzFw