{"id":123950,"date":"2021-06-18T15:23:09","date_gmt":"2021-06-18T22:23:09","guid":{"rendered":"https:\/\/lifeboat.com\/blog\/2021\/06\/mathematicians-welcome-computer-assisted-proof-in-grand-unification-theory"},"modified":"2021-06-18T15:23:09","modified_gmt":"2021-06-18T22:23:09","slug":"mathematicians-welcome-computer-assisted-proof-in-grand-unification-theory","status":"publish","type":"post","link":"https:\/\/lifeboat.com\/blog\/2021\/06\/mathematicians-welcome-computer-assisted-proof-in-grand-unification-theory","title":{"rendered":"Mathematicians welcome computer-assisted proof in grand unification theory"},"content":{"rendered":"

<\/a><\/p>\n

Once researchers have done the hard work of translating a set of mathematical concepts into a proof assistant, the program generates a library of computer code that can be built on by other researchers and used to define higher-level mathematical objects. In this way, proof assistants can help to verify mathematical proofs that would otherwise be time-consuming and difficult, perhaps even practically impossible, for a human to check.<\/p>\n

Proof assistants have long had their fans, but this is the first time that they have played a major role at the cutting edge of a field, says Kevin Buzzard, a mathematician at Imperial College London who was part of a collaboration that checked Scholze and Clausen\u2019s result. \u201cThe big remaining question was: can they handle complex mathematics?\u201d Says Buzzard. \u201cWe showed that they can.\u201d<\/p>\n

And it all happened much faster than anyone had imagined. Scholze laid out his challenge<\/a> to proof-assistant experts in December 2020, and it was taken up by a group of volunteers led by Johan Commelin, a mathematician at the University of Freiburg in Germany. On 5 June \u2014 less than six months later \u2014 Scholze posted on Buzzard\u2019s blog<\/a> that the main part of the experiment had succeeded. \u201cI find it absolutely insane that interactive proof assistants are now at the level that, within a very reasonable time span, they can formally verify difficult original research,\u201d Scholze wrote.<\/p>\n","protected":false},"excerpt":{"rendered":"

Once researchers have done the hard work of translating a set of mathematical concepts into a proof assistant, the program generates a library of computer code that can be built on by other researchers and used to define higher-level mathematical objects. In this way, proof assistants can help to verify mathematical proofs that would otherwise [\u2026]<\/p>\n","protected":false},"author":396,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1523,2229],"tags":[],"class_list":["post-123950","post","type-post","status-publish","format-standard","hentry","category-computing","category-mathematics"],"_links":{"self":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/posts\/123950","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/users\/396"}],"replies":[{"embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/comments?post=123950"}],"version-history":[{"count":0,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/posts\/123950\/revisions"}],"wp:attachment":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/media?parent=123950"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/categories?post=123950"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/tags?post=123950"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}