Mathematics Department Colloquium: Interactive Theorem Proving

Colloquium | February 13 | 4:10-5 p.m. | 60 Evans Hall

 Scott Morrison, Mathematical Sciences Institute of the Australian National University

 Department of Mathematics

Today we use computers to communicate mathematics (e.g., email, arXiv, MathOverflow), as well as to compute and explore (e.g., with computer algebra systems). Nevertheless the role of computers in constructing, understanding, and verifying proofs is relatively limited in practice. Certain long proofs have been formally verified (e.g., the four colour theorem, the Kepler conjecture, and the odd order theorem). However these arguments are far from most mathematicians' usual interests, and there was an enormous logistical overhead in preparing these formal proofs.

New software tools, and the communities springing up around these, may introduce a new period in mathematics when researchers routinely collaborate with the computer. We're not there yet! Nevertheless, with sufficiently low technical barriers to communication between human and computer, and with good tools to quickly codify human heuristics and leverage machine learning, interactive theorem provers may soon help rather than hinder.

This talk will give a quick tour of where we stand at the moment. I'll highlight the new language Lean, and the community of mathematicians and computer scientists using it. I'll give a demo, and mention some recent advances. (Lean knows what a perfectoid space is! Simple machine learning helps searching for rewriting proofs! Lean wants to compete in the IMO!)

 ribet@berkeley.edu