Microsoft Research334 тыс
Опубликовано 27 октября 2022, 15:35
Digitization of mathematics is a nascent concept. Historically, technical achievements have been gatekept by peer validation, keeping the upper most levels of the field exclusive and causing a trust bottleneck in novel explorations. Microsoft Research’s programming language and proof assistant Lean is eliminating the bottleneck by digitizing mathematics and enabling computers to verify mathematical theorems. Lean has flourished in the mathematical community and empowered users of all levels to grow their expertise, using Lean as their teacher. Join Leonardo de Moura (Microsoft Research), Jeremy Avigad (Carnegie Mellon University), and Heather Macbeth (Fordham University) in a series of lightning talks covering the digital revolution happening in mathematics, the widening adoption of Lean as a proof assistant, and how Lean is democratizing education.
#MSFTResearchSummit
See related sessions in this track: microsoft.com/en-us/research/v...
Learn more about the 2022 Microsoft Research Summit: microsoft.com/en-us/research/e...
#MSFTResearchSummit
See related sessions in this track: microsoft.com/en-us/research/v...
Learn more about the 2022 Microsoft Research Summit: microsoft.com/en-us/research/e...
Свежие видео
Случайные видео