Proof formalization in Lean, or how to trick a computer into doing (even more) math for you!

event Tuesday, April 9, 2024
access_time 6:00pm (CDT)
room PHSC 1105
info Pizza and drinks will be provided.

Abstract: Since computers were invented, mathematicians do not have to spend hours doing computations, and can use their time to write proofs- which they need to check and double-check. What if they could also use computers to help with this? They would have more time to drink coffee! Lean is a functional programming language that allows you to write theorems and proofs, and it verifies whether they are correct. In this session, we will have fun learning the basics about Lean while playing a game! Please, bring your own computer (you don’t need to install anything).

For more information on this event, please contact Anuradha Ekanayake.