Una de las líneas de trabajo en la automatización del razonamiento es la verificación de demostraciones de grandes teoremas. En esta línea se inscribe el proyecto de la formalización en Coq del teorema clasificación de grupos finitos. Un resultado clave para dicha demostración es el teorema de Feit y Thompson, también conocido como el teorema del orden impar. Recientemente se ha conseguido la formalización del teorema en Coq como se comenta en el artículo A machine-checked proof of the odd order theorem.
Sus autores son Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi y Laurent Théry.
Su resumen es
This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq. To support the formalization, we developed a comprehensive set of reusable libraries of formalized mathematics, including results in finite group theory, linear algebra, Galois theory, and the theories of the real and complex algebraic numbers.
Las conclusiones del trabajo son
The success of the present formalization relies on a heavy use of the inductive types provided by Coq and on various flavors of reflection techniques. A crucial ingredient was the transfer of the methodology of “generic programming” to formal proofs, using the type inference mechanisms of the Coq system.
Our development includes more than 150,000 lines of proof scripts, including roughly 4,000 definitions and 13,000 theorems. The roughly 250 pages of mathematics in our two main sources translate to about 40,000 lines of formal proof, which amounts to 4-5 lines of SSReflect code per line of informal text. During the formalization, we had to correct or rephrase a few arguments in the texts we were following, but the most time-consuming part of the project involved getting the base and intermediate libraries right. This required systematic consolidation phases performed after the production of new material. The corpus of mathematical theories preliminary to the actual proof of the Odd Order theorem represents the main reusable part of this work, and contributes to almost 80 percent of the total length. Of course, the success of such a large formalization, involving several people at different locations, required a very strict discipline, with uniform naming conventions, synchronization of parallel developments, refactoring, and benchmarking for synchronization with Coq.
As we have tried to make clear in this paper, when it comes to formalizing this amount of mathematics, there is no silver bullet. But the combined success of the many techniques we have developed shows that we are now ready for theorem proving in the large. The outcome is not only a proof of the Odd Order Theorem, but also, more importantly, a substantial library of mathematical components, and a tried and tested methodology that will support future formalization efforts.
Una vesión minimal de la demostración en Coq del teorema del orden impar se encuentra aquí. La formalización completa se encuentra aquí.