Formal Theorem Proving with Lean

featuring Alex Kontorovich

Wednesday, October 16
6:30 pm to 7:30 pm

(in person)

Interactive Theorem Proving software, such as the Lean proof assistant, is becoming an increasingly important tool with numerous applications, both to theoretical research mathematics and in the real world (for example, in AI systems such as the recent DeepMind project that claimed a Silver Medal for the International Mathematical Olympiad).  It also has the potential to become an extremely valuable tool for mathematics education to help train young learners on the skill of rigorous thinking.  Join Alex Kontorovich, a Distinguished Professor of Mathematics at Rutgers University, for a gentle introduction to this technology, aimed at a general audience.

This presentation is appropriate for students ages 12 and older, and anyone who knows or is ready to learn the principle of mathematical induction.