CMSA Seminar AI for the working mathematician: An Informal Introduction to Formal Proofs

In this talk we will give an introduction to Lean, a programming language adapted to expressing and verifying proofs. Lean and its flagship library, mathlib, have been the focus of a dedicated user community for about a decade, but their visibility has grown significantly in the last year. This is in large part because Lean makes validating large AI-generated proofs dramatically more practical: the human work is reduced from analyzing the logical correctness of an entire proof to analyzing the semantic correctness of a Lean statement. The main goal of the talk will be to build some example-based intuition for how this works in practice. Time permitting, we will also discuss how Lean interacts with the way modern AI systems are trained, and potential implications of formal theorem proving for the broader interaction between science and mathematics.

We hope you will join us in G10 in the basement of CMSA, 20 Garden Street. The seminar will also be broadcast online at the same time at the following zoom link.

https://harvard.zoom.us/j/94536195785?pwd=HpTRZMq5zxgHK8ODc25aWV7Lcx1TSC.1
Meeting ID: 945 3619 5785
Password: cmsa