Notice:
This event occurs in the past.
School Colloquium by Dr. Kevin Cheung
Friday, February 13, 2026 from 3:30 pm to 4:30 pm
- In-person event
- HP 4351, Macphail Room, Herzberg Building, 4th floor, Herzberg Laboratories, Carleton University
- 1125 Colonel By Drive, Ottawa, ON, K1S 5B6
The School of Mathematics and Statistics will be holding a Colloquium on Friday, February 13, 2026.
- Title: Leaning Towards Formal Proofs
- Speaker: Dr. Kevin Cheung, School of Mathematics and Statistics, Carleton University
- Abstract: In recent years, there has been increasing interest among mathematicians in using the Lean interactive theorem prover to develop formal proofs. In this talk, I will give a brief introduction to Lean and share some personal experiences using the system.