Microsoft Research Lean Award Program
Region: Global
Advancing Lean as a functional programming language and mathematical theorem prover
Status: Closed for academic year 2023
About the program
(opens in new tab)The Microsoft Research Lean Award is an award given to those advancing the growth of Lean as a functional programming language and mathematical theorem prover (opens in new tab).
Our mission is to revolutionize mathematics by empowering anyone with an interest to grow in the field, using the Lean programming language and theorem prover as the catalyst. Microsoft Research collaborates with the academic community in pursuit of our mission to democratize mathematics, accelerate the frontiers of mathematical research, and improve equal access to math education. The Microsoft Research Lean Award is given to any person or organization demonstrating strong advocacy for our mission objectives and Lean, with the intention that the award will boost recipients’ stewardship efforts for Lean during the academic year.
2023 Academic year award recipients
This year’s awards were gifted to four mathematicians who emerged as leaders in the Lean community. Award recipients were instrumental in maintaining Lean’s Mathematical Library (MathLib), championed Lean in their own areas of academic research, and provided proposals to expand their work in both research and undergraduate teaching curriculums using Lean.
Johan Commelin
University of Freiburg
Johan Commelin is a mathematician specializing in arithmetic geometry. Since 2018, he has used Lean to formally verify mathematics. In the last two years, he has focused on formalization of condensed mathematics, and in particular the main theorem of liquid vector spaces. Johan’s formalization work with brand-new mathematics is pushing the boundaries of what interactive theorem provers can do.
With the Microsoft Research Lean Award, Johan will be able to hire a postdoc to work on improving the way that isomorphism-invariance can be handled in formal mathematics using Lean. They will take inspiration from homotopy type theory and sheaf-theoretic methods that were formalized in a project on model theory.
Rob Lewis
Brown University
Rob Lewis is a lecturer in the CS department at Brown University. He has been involved in the Lean community since 2014 when he worked on a classical analysis library in Lean 2 and is a MathLib maintainer. His research focuses on how tactics and metaprograms in Lean can be used to create an experience more like traditional mathematics.
The Microsoft Research Lean Award will enable Rob to fully incorporate Lean into the Discrete Structures and Probability course he teaches at Brown – an intermediate course that introduces CS students to topics in discrete mathematics. The use of Lean as the proof assistant will help emphasize the formal grammar of mathematical statements, the structure of proofs, and connections between math and computer science.
Heather Macbeth
Fordham University
Heather Macbeth is an assistant professor of mathematics at Fordham University, specializing in differential geometry. She obtained a Ph.D. from Princeton and was previously a postdoc at MIT and at the ENS. She has been a MathLib maintainer since 2020 and works on formalization projects in analysis and geometry. She also experiments with using Lean for teaching undergraduate mathematics.
The Microsoft Research Lean Award will support Heather’s work on the formalization of foundations of the theory of partial differential equations, the preparation of a new undergraduate level Fordham course using Lean, and regular MathLib maintenance, via a teaching reduction for Heather and summer stipends for Fordham students working on Lean projects. The award will also support travel to connect with the Lean community.
Patrick Massot
University Paris-Saclay, Orsay
Patrick Massot is a professor of mathematics at University Paris-Saclay in Orsay. His original field of research is contact and symplectic topology, but he is currently exploring the boundary between geometrical flexibility and rigidity. He began using Lean in 2017 to check his computations when he became interested in formalized mathematics, and quickly realized the potential. He now is an avid Lean user for both research and teaching.
The Microsoft Research Lean Award Patrick received will be used to fund a one-year post-doc position in Orsay focusing on formalization of mathematics. They will ensure that MathLib contains everything necessary for an undergraduate course, develop ways to turn MathLib into teaching material, and create interactive documents for Lean via metaprogramming. Readers will be able to choose the level of detail, from an informal sketch to proof terms, with smooth transitions.