{"id":302408,"date":"2012-10-11T09:30:35","date_gmt":"2012-10-11T16:30:35","guid":{"rendered":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/?p=302408"},"modified":"2016-10-12T11:36:26","modified_gmt":"2016-10-12T18:36:26","slug":"theorem-proof-gains-acclaim","status":"publish","type":"post","link":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/blog\/theorem-proof-gains-acclaim\/","title":{"rendered":"Theorem Proof Gains Acclaim"},"content":{"rendered":"<p><em>By Rob Knies, Managing Editor, Microsoft Research<\/em><\/p>\n<p>At 5:46 p.m. on Sept. 20, Georges Gonthier, principal researcher at <a href=\"https:\/\/newed.any0.dpdns.org\/en-us\/research\/lab\/microsoft-research-cambridge\/\" target=\"_blank\">Microsoft Research Cambridge<\/a>, sent a brief email to his colleagues at the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.msr-inria.inria.fr\/\" target=\"_blank\">Microsoft Research-Inria Joint Centre<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> in Paris. It read, in full:<\/p>\n<p>\u201cThis is really the End.\u201d<\/p>\n<div id=\"attachment_302411\" style=\"width: 320px\" class=\"wp-caption alignright\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-302411\" class=\"size-full wp-image-302411\" src=\"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-content\/uploads\/2016\/10\/Georges-Gonthier.png\" alt=\"Georges Gonthier\" width=\"310\" height=\"250\" srcset=\"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-content\/uploads\/2016\/10\/Georges-Gonthier.png 310w, https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-content\/uploads\/2016\/10\/Georges-Gonthier-300x242.png 300w\" sizes=\"auto, (max-width: 310px) 100vw, 310px\" \/><p id=\"caption-attachment-302411\" class=\"wp-caption-text\">Georges Gonthier<\/p><\/div>\n<p>Those five innocuous words heralded the culmination of a project that had consumed more than six years and resulted in the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.msr-inria.fr\/news\/feit-thomson-proved-in-coq\/\" target=\"_blank\">formal proof of the Feit-Thompson Theorem<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, the first major step of the classification of finite simple groups.<\/p>\n<p>The theorem, first proved by Walter Feit and John Griggs Thompson in 1963 and also known as the Odd-Order Theorem, states that in mathematical group theory, every finite group of odd order is solvable.<\/p>\n<p>That might seem a deceptively simple definition to non-mathematicians, but Gonthier and his collaborators on the Mathematical Components project at the Microsoft Research-INRIA Joint Centre are anything but. Their achievement in completing a computer-assisted proof by the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/coq.inria.fr\/what-is-coq\" target=\"_blank\">Coq proof assistant<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, developed at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.inria.fr\/en\/\" target=\"_blank\">Inria<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, the French National Research Institute for Computer Science and Applied Mathematics, was acclaimed widely as news spread.<\/p>\n<p>Michel Cosnard, Inria chairman of the board and CEO, was quick to commend the development.<\/p>\n<p>\u201cMy deepest congratulations for this beautiful and amazing piece of work,\u201d he wrote. \u201cOf course, Georges Gonthier and his team deserve our full consideration. But I would also underline the quality of the Microsoft Research-Inria partnership, which gave to them the absolutely necessary conditions for climbing this Everest.\u201d<\/p>\n<p>Andrew Blake, laboratory director at Microsoft Research Cambridge, provided further detail:<\/p>\n<p>\u201cGeorges and his team at Inria have been working on this proof of the Feit-Thompson or Odd-Order Theorem for six years or so, since he completed his proof of the Four-Color Theorem. That might seem a long time for one theorem, but in fact:<\/p>\n<ul>\n<li>\u201cIt is a big theorem\u2014the proof runs to two volumes. This is a large body of material to verify by eye\u2014how much confidence can one have in that? Now the verification is substantially automated through the use of Coq.<\/li>\n<li>\u201cAlong the way, a good deal of the structure of finite-group theory\u2014textbooks of standard results\u2014have been coded and verified.<\/li>\n<li>\u201cAll of this has also stressed the Coq proof environment and strengthened it, and Coq is also used for a multitude of verification tasks in security-critical code.<\/li>\n<\/ul>\n<p>\u201cOne may anticipate that this could affect profoundly both computer science and mathematics.\u201d<\/p>\n<p>As Blake mentioned, Gonthier, winner of the <a href=\"https:\/\/newed.any0.dpdns.org\/en-us\/research\/gonthier-earns-eads-foundation-honor\/\" target=\"_blank\">2011 EADS Foundation Grand Prize in Computer Science<\/a>, is no stranger to this sort of achievement. In 2005, he and Benjamin Werner completed a formal proof of the Four-Color Theorem, the first longstanding mathematical problem to be resolved using a computer program. In <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf\" target=\"_blank\"><em>Formal Proof\u2014The Four Color Theorem<\/em><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, published in December 2008 in <em>Notices of the American Mathematical Society<\/em>, Gonthier explained what was at stake.<\/p>\n<p>\u201cFor some 30 years,\u201d he wrote, \u201ccomputer science has been working out a solution to this problem: formal program proofs. The idea is to write code that describes not only <em>what<\/em> the machine should do, but also <em>why<\/em> it should be doing it\u2014a formal proof of correctness. The validity of the proof is an objective mathematical fact that can be checked by a <em>different<\/em> program, whose own validity can be ascertained empirically because it does run on <em>many<\/em> inputs.<\/p>\n<p>\u201cThe main technical difficulty is that formal proofs are very difficult to produce, even with a language rich enough to express all mathematics.\u201d<\/p>\n<p>Now that he and his team have achieved a second mathematical theorem completely proved in Coq, he explains the background behind the six-year effort.<\/p>\n<p>\u201cGroups are very important objects in mathematics,\u201d Gonthier says. \u201cThey describe sets of symmetries, or reversible operations, and they have been used to explain the structure of nature, specifically how atomic particles combine and fall into various classes. They\u2019re also well-known in computer science, because group theory is the base for most cryptography schemes.\u201d<\/p>\n<p>To illustrate the concept of \u201cgroup,\u201d he refers to a common but challenging brainteaser.<\/p>\n<p>\u201cThink about a Rubik\u2019s Cube,\u201d Gonthier says. \u201cIt is a puzzle based on group theory, because the various operations you do when you turn the cubes around can all be reversed. If you do a couple of them, it all seems mixed up. But if you know a little group theory, you understand how to solve the cube.<\/p>\n<p>\u201cThe Odd-Order Theorem precisely says that groups that have an odd number of elements are solvable. Finite groups can be factored somewhat like integers, though for a more complicated multiplication. The basic group factors, called simple groups, also come in many more shapes than the basic integer factors, the prime numbers. Solvable groups, however, can be factored down to primes, like integers. They\u2019re called this because they correspond to solvable polynomial equations.\u201d<\/p>\n<h2>Innovation at Length<\/h2>\n<p>The proof by Feit and Thompson showed that groups with an odd number of elements are always solvable. It was shocking to the mathematical community at the time, because the proof lasted for 255 pages, a gargantuan effort that has proved to be quite mathematically innovative.<\/p>\n<p>Now with the formal, computer-checked proof of the Feit-Thompson Theorem, Gonthier and collaborators, most notably Assia Mahboubi and Laurent Th\u00e9ry of Inria, have extended the utility of the theorem.<\/p>\n<p>\u201cBecause the formal proof can be computer-processed,\u201d Gonthier says, \u201cwe can get more information out of it. We can know that it\u2019s absolutely correct.\u201d<\/p>\n<p>Gonthier describes his initial emotion upon completing the formal proof as \u201celation\u201d and reports that he immediately began to contemplate a full night\u2019s sleep, which had proved difficult to obtain as the effort grew to a close. But clearly, it was a passionate pursuit.<\/p>\n<p>\u201cThe work is about developing the use of computers as tools for doing mathematics for processing mathematical knowledge,\u201d he says. \u201cMathematics is one of the last great romantic disciplines, where basically one genius has to hold everything in his head and understand everything all at once.<\/p>\n<p>\u201cComputers have been gaining in math, but mostly to solve ancillary problems such as type setting, or carrying out numerical or symbolic calculation, or enumerating various categories of common natural objects, like polyhedra of various shapes. They\u2019re not used to process the actual mathematical knowledge: the theories, the definitions, the theorems, and the proofs of those theorems.\u201d<\/p>\n<p>The possibility of doing so has been tantalizing but elusive.<\/p>\n<p>\u201cMy work has been to try to break this barrier and make computers into effective tools,\u201d Gonthier states. \u201cThat is mostly about finding ways of expressing mathematical knowledge so that it can be processed by software.\u201d<\/p>\n<p>The focus of the project was on developing tools for expressing mathematics.<\/p>\n<h2>One Step at a Time<\/h2>\n<p>\u201cUltimately, there were a number of intermediate goals in developing a good theory,\u201d Gonthier says, \u201cfirst of all, observing pen-and-paper mathematics. I had much of that done by the time I\u2019d completed the proof of the Four-Color Theorem. Then it was basic group theory, then algebra, then more advanced group theory, then character theory, and so on. There were lots of intermediate objectives, and we\u2019d just move from one target to the next.\u201d<\/p>\n<p>When Gonthier first suggested a formal Feit-Thompson Theorem proof, his fellow members of the Mathematical Components team at Inria could hardly believe their ears.<\/p>\n<p>\u201cThe reaction of the team the first time we had a meeting and I exposed a grand plan,\u201d he recalls ruefully, \u201cwas that I had delusions of grandeur. But the real reason of having this project was to understand how to build all these theories, how to make them fit together, and to validate all of this by carrying out a proof that was clearly deemed to be out of reach at the time we started the project.\u201d<\/p>\n<p>Along the way, he learned a few things\u2014about formal proofs in group theory and about himself.<\/p>\n<p>\u201cStubbornness pays off,\u201d he laughs, before reflecting on how the latest proof differed from his work on the Four-Color Theorem.<\/p>\n<p>\u201cThe Four-Color Theorem proof I basically did on my own,\u201d Gonthier says. \u201cHere, I worked with a team in more of a leadership role, and motivating the team was a new challenge for me.\u201d<\/p>\n<p>Apparently, he proved sufficiently motivating. A couple of hours after Gonthier sent his original mail, Th\u00e9ry sent his own, providing a few facts about the project:<\/p>\n<p>\u201cNumber of lines\u2014170,000,\u201d he wrote. \u201cNumber of definitions\u201415,000. Number of theorems\u20144,300. Fun\u2014enormous!\u201d<\/p>\n<p>Initial enthusiasm aside, though, the hope is that the formal proof of the Feit-Thompson Theorem could lead to similarly big results in proofs of programs.<\/p>\n<p>\u201cThe Feit-Thompson Theorem,\u201d Gonthier says, \u201cis the first steppingstone in a much larger result, the classification of finite simple groups, which is known as the \u2018monster theorem\u2019 because it\u2019s one of those theorems where belief in it resides in the belief of a few selected people who have understanding of it.\u201d<\/p>\n","protected":false},"excerpt":{"rendered":"<p>By Rob Knies, Managing Editor, Microsoft Research At 5:46 p.m. on Sept. 20, Georges Gonthier, principal researcher at Microsoft Research Cambridge, sent a brief email to his colleagues at the Microsoft Research-Inria Joint Centre in Paris. It read, in full: \u201cThis is really the End.\u201d Those five innocuous words heralded the culmination of a project [&hellip;]<\/p>\n","protected":false},"author":39507,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[194483],"tags":[213983,213986,201565,213992,213989,213980,196479,213977],"research-area":[13546],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-302408","post","type-post","status-publish","format-standard","hentry","category-mathematics","tag-computer-assisted-proof","tag-coq-proof-assistant","tag-feit-thompson-theorem","tag-finite-group-theory","tag-four-color-theorem","tag-mathematical-components-project","tag-microsoft-research-inria-joint-centre","tag-odd-order-theorem","msr-research-area-computational-sciences-mathematics","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[199561],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-events":[],"related-researchers":[],"msr_type":"Post","byline":"","formattedDate":"October 11, 2012","formattedExcerpt":"By Rob Knies, Managing Editor, Microsoft Research At 5:46 p.m. on Sept. 20, Georges Gonthier, principal researcher at Microsoft Research Cambridge, sent a brief email to his colleagues at the Microsoft Research-Inria Joint Centre in Paris. It read, in full: \u201cThis is really the End.\u201d&hellip;","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/posts\/302408","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/users\/39507"}],"replies":[{"embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/comments?post=302408"}],"version-history":[{"count":5,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/posts\/302408\/revisions"}],"predecessor-version":[{"id":304634,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/posts\/302408\/revisions\/304634"}],"wp:attachment":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/media?parent=302408"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/categories?post=302408"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/tags?post=302408"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=302408"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=302408"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=302408"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=302408"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=302408"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=302408"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=302408"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=302408"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}