The Future of Mathematics?
As a professor of pure mathematics, my job involves teaching, research, and outreach. Two years ago I got interested in formal methods, and I learned how to use the Lean theorem prover developed at MSR. Since then I have become absolutely convinced that tools like Lean will play a role in the future of mathematics. With the help of a team of enthusiastic undergraduates at my university, we have begun to digitize our curriculum using Lean, and things are moving very fast. I will talk about our achievements, as well as the issues and challenges that we have faced. Reaching the staff has proved harder because these tools are not currently mature enough to be a useful tool for high-level mathematical research. I believe that this situation will inevitably change. Mathematician Tom Hales, famous for proving the Kepler conjecture, has a project called Formal Abstracts which will ultimately offer several new tools to research mathematicians. Hales has chosen to use Lean as the back end for his project. I will finish by discussing his vision, my thoughts on the construction of the tools I am convinced we can make, and finally I will speculate on the future of mathematics.
No advanced mathematical knowledge will be assumed.
Speaker Details
Kevin Buzzard studied as an undergraduate and PhD student at the University of Cambridge, England, and was a post-doc at UC Berkeley. He is currently a professor of pure mathematics at Imperial College London, having had visiting positions at Harvard, Cambridge, the IAS in Princeton and the IHP in Paris. He was awarded a Whitehead Prize by the London Mathematical Society in 2002 for “his distinguished work in number theory”, and the Senior Berwick Prize in 2008.
- Date:
- Speakers:
- Kevin Buzzard
- Affiliation:
- Imperial College London
