{"id":915084,"date":"2023-02-15T12:02:14","date_gmt":"2023-02-15T20:02:14","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&p=915084"},"modified":"2023-02-15T12:02:16","modified_gmt":"2023-02-15T20:02:16","slug":"lean","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/lean\/","title":{"rendered":"Lean"},"content":{"rendered":"
\n\t
\n\t\t
\n\t\t\t\"mathematical\t\t<\/div>\n\t\t\n\t\t
\n\t\t\t\n\t\t\t
\n\t\t\t\t\n\t\t\t\t
\n\t\t\t\t\t\n\t\t\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\n\n

Lean<\/h1>\n\n\n\n

Programming language and theorem prover<\/p>\n\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/div>\n<\/section>\n\n\n\n\n\n

What is Lean?<\/h2>\n\n\n\n
\"LEAN<\/figure>\n\n\n\n

Lean is a functional programming language and interactive theorem prover. Our project strives to revolutionize mathematics by empowering anyone with an interest to grow in the field using Lean as their assistant. Lean was developed by Microsoft Research in 2013 as an initial effort to help mathematicians and engineers solve complex math problems. Lean is an open-source development environment for formal mathematics, also known as machine-checkable mathematics, used by and contributed to by an active community of mathematicians around the world.<\/p>\n\n\n\n

The digital revolution has been driven by mathematical innovation. The complexity of mathematical problems is increasing massively. Yet today\u2019s math is hard to referee, seldom read, or cited. We now have proofs that cannot be manually refereed. Collaboration in math is difficult and still limited to small groups. Historically, technical achievements through verified proofs have been gatekept by peer validation, keeping the upper most levels of the field exclusive and causing a trust bottleneck in novel explorations. Deconstructing the thought process used to achieve a result into widely checkable commentary is fertile for introductory methods. Lean is eliminating the bottleneck by digitizing mathematics and enabling computers to verify mathematical theorems. We are building the platform for the next wave of mathematicians to embrace formal mathematics.<\/p>\n\n\n\n

Microsoft Research collaborates with the academic and Lean community in pursuit of our mission to democratize mathematics, accelerate the frontiers of mathematical research, and improve equal access to math education. Our community of students, professors, and mathematicians actively contribute to Lean\u2019s mathematical library (Mathlib (opens in new tab)<\/span><\/a>). The community has digitized over half of the undergraduate mathematics curriculum into Lean as well as concepts at the frontiers of mathematics (such as Perfectoid Spaces) and is over one million lines of code. The community\u2019s goal is to reach 10 million lines of code in the next five years to completely digitize the undergraduate mathematics curriculum and further the progress of formalized proofs, such as Fermat\u2019s Last Theorem. Lean has already demonstrated its potential to revolutionize and radically accelerate mathematics, for example, helping Fields Medalist Peter Scholze confirm a new theorem in the Liquid Tensor Experiment (opens in new tab)<\/span><\/a>. At Microsoft Research, we are working on the algorithms, data structures, and proof automation for the Lean platform to support a digital library of this scale effectively and greatly reduce formal mathematics overhead. We will claim the formal mathematics revolution is complete by reaching a de Bruijn factor of 1, when the ratio of proof length in Lean is equal to the proof length in mathematical prose. We believe Lean is spearheading the formal mathematics revolution and will empower the next generation of mathematicians to prove major open conjectures previously deemed impossible.<\/p>\n\n\n\n

\n
<\/div>\n\n\n\n
<\/div>\n\n\n\n
<\/div>\n<\/div>\n\n\n\n
\n
\n
\n