{"id":888408,"date":"2022-10-24T09:00:28","date_gmt":"2022-10-24T16:00:28","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-video&#038;p=888408"},"modified":"2022-10-25T06:00:38","modified_gmt":"2022-10-25T13:00:38","slug":"lightning-talks-empowering-mathematicians-with-technology","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/lightning-talks-empowering-mathematicians-with-technology\/","title":{"rendered":"Lightning talks: Empowering mathematicians with technology"},"content":{"rendered":"<p>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\u2019s 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.<\/p>\n<p><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/microsoft-research-summit-2022\/\">Learn more about the 2022 Microsoft Research Summit ><\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>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\u2019s programming language and proof assistant Lean is eliminating the bottleneck by digitizing mathematics and enabling computers to verify mathematical theorems. [&hellip;]<\/p>\n","protected":false},"featured_media":888411,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13546],"msr-video-type":[266190,266181],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[261667],"msr-pillar":[],"class_list":["post-888408","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-research-area-computational-sciences-mathematics","msr-video-type-amplifying-human-productivity-and-creativity","msr-video-type-microsoft-research-summit-2022","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/esNKOKeveRE","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/888408","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/888408\/revisions"}],"predecessor-version":[{"id":888420,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/888408\/revisions\/888420"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/888411"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=888408"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=888408"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=888408"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=888408"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=888408"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=888408"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=888408"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}