Events
DMS Colloquium: Chris Kapulkin |
| Time: Aug 30, 2024 (04:00 PM) |
| Location: 010 ACLC |
|
Details: Refreshments will be served in Parker 244, 3:30-3:55p.m.
Please note that this talk is not affected by a recent change in colloquia schedule and will be held on Friday.
 Speaker: Chris Kapulkin (University of Western Ontario).
Title: Interactive Theorem Proving
Abstract: For many years, mathematicians have used computers to perform computations that inform their research and lead to new conjectures. More recently, computers have been used to formally verify correctness of proofs via software known as proof assistants. This talk will be an introduction to proof assistants - what they are, why they are used, and what the mathematical community has accomplished with them. A short introduction to the most commonly used proof assistant, Lean, will also be given. Together, we will use Lean to formally verify that every natural number is either even or odd, a fact that shouldn't surprise many but is a good illustration of what working with a proof assistant is like. Those interested in following the proof on their own computers are encouraged to install Lean ahead of the talk by going to: The process is straightforward and will certainly help get the most out of the talk.
Faculty host: Selim Sukhtaiev
|