Formalizing Mathematics in Lean

Author(s)
Greg
Baimetov
*,
University of Washington
Talk Abstract
Proof assistants such as Lean have taken on an increasing role in Mathematics, even now being used to verify the correctness of difficult theorems in modern mathematics. This talk aims to introduce the Lean proof assistant, its applications to mathematics and other fields, and the speaker's personal experience with it.
Talk Subject
Mathematical Aspects of Computer Science
Time Slot
2023-11-11T14:40:00
Room Number
2