{"id":792806,"date":"2021-11-16T08:00:31","date_gmt":"2021-11-16T16:00:31","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&#038;p=792806"},"modified":"2021-11-18T07:07:57","modified_gmt":"2021-11-18T15:07:57","slug":"lightning-talks-augmented-mathematical-intelligence","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/lightning-talks-augmented-mathematical-intelligence\/","title":{"rendered":"Lightning talks: Augmented Mathematical Intelligence"},"content":{"rendered":"<p>Augmented Mathematical Intelligence (AMI) refers to the ability to solve formally specified problems as reliably as humans can over all classes of such problems that are of interest to our civilization. This includes not only mathematics but also computer science, cryptography, and statistics, for example. AMI also includes many subproblems arising in software engineering, physics, finance, and possibly even law. Whereas Artificial General Intelligence (AGI) is both philosophically ill-posed and arbitrarily out of reach, we see a relatively concrete path to reaching AMI using near-future technology on top of the Lean Proof Assistant, an open-source Microsoft Research project. AMI is merely a tool without agency, and does not aim to replace human judgment or aesthetics. Instead, AMI will empower humans to innovate more and with less onerous training.<\/p>\n<p><strong>Related:<\/strong><\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/leanprover.github.io\/about\/\" target=\"_blank\" rel=\"noopener\">https:\/\/leanprover.github.io\/about\/<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/dselsam\" target=\"_blank\" rel=\"noopener\">https:\/\/github.com\/dselsam<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/x.com\/leanprover\" target=\"_blank\" rel=\"noopener\">https:\/\/x.com\/leanprover<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/stacks.math.columbia.edu\/\" target=\"_blank\" rel=\"noopener\">https:\/\/stacks.math.columbia.edu\/<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>Learn more about the 2021 Microsoft Research Summit: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/Aka.ms\/researchsummit\">https:\/\/Aka.ms\/researchsummit<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Augmented Mathematical Intelligence (AMI) refers to the ability to solve formally specified problems as reliably as humans can over all classes of such problems that are of interest to our civilization. This includes not only mathematics but also computer science, cryptography, and statistics, for example. AMI also includes many subproblems arising in software engineering, physics, [&hellip;]<\/p>\n","protected":false},"featured_media":792809,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13546,13560],"msr-video-type":[261305,261263],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-792806","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-research-area-computational-sciences-mathematics","msr-research-area-programming-languages-software-engineering","msr-video-type-empowering-software-developers-and-mathematicians-with-next-generation-ai","msr-video-type-research-summit-2021","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/6_nLj9OnbDg","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/792806"}],"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":3,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/792806\/revisions"}],"predecessor-version":[{"id":797914,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/792806\/revisions\/797914"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/792809"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=792806"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=792806"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=792806"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=792806"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=792806"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=792806"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=792806"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}