The Future of Mathematics?

Channel:
Microsoft Research
Subscribers:
351,000
Published on ● Video Link: https://www.youtube.com/watch?v=Dp-mQ3HxgDE


Duration: 1:14:48
93,585 views
2,627

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.

Talk slides: https://www.microsoft.com/en-us/research/uploads/prod/2019/09/The-Future-of-Mathematics-SLIDES.pdf

Learn more about this and other talks at Microsoft Research: https://www.microsoft.com/en-us/research/video/the-future-of-mathematics/



Other Videos By Microsoft Research


2019-10-11HapSense: A Soft Haptic I/O Device with Uninterrupted Dual Functionalities...
2019-10-09Advanced polarized light microscopy for mapping molecular orientation
2019-10-09Data science and ML for human well-being with Jina Suh [Podcast]
2019-10-07Tea: A High-level Language and Runtime System for Automating Statistical Analysis [Python module]
2019-10-07Discover[i]: Component-based Parameterized Reasoning for Distributed Applications
2019-10-04Scheduling For Efficient Large-Scale Machine Learning Training
2019-10-03Distributed Entity Resolution for Computational Social Science
2019-10-03MMLSpark: empowering AI for Good with Mark Hamilton [Podcast]
2019-10-02Non-linear Invariants for Control-Command Systems
2019-10-02Vision-and-Dialog Navigation
2019-10-01The Future of Mathematics?
2019-09-30How Not to Prove Your Election Outcome
2019-09-30The Worst Form Including All Those Others: Canada’s Experiments with Online Voting
2019-09-30DIFF: A Relational Interface for Large-Scale Data Explanation
2019-09-30A Calculus for Brain Computation
2019-09-26Decoding Multisensory Attention from Electroencephalography for Use in a Brain-Computer Interface
2019-09-26A Short Introduction to DIMACS & DIMACS and MSR-NYC
2019-09-26Boosting Innovation and Discovery of Ideas
2019-09-26Resource-Efficient Redundancy for Large-Scale Data Processing and Storage Systems
2019-09-26Optimizing Declarative Graph Queries at Large Scale
2019-09-25SILK: Preventing Latency Spikes in Log-Structured Merge Key-Value Stores