A Machine-Checked Proof of the Odd Order TheoremReportar como inadecuado

A Machine-Checked Proof of the Odd Order Theorem - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

* Corresponding author 1 MSR - INRIA - Microsoft Research - Inria Joint Centre 2 MARELLE - Mathematical, Reasoning and Software CRISAM - Inria Sophia Antipolis - Méditerranée 3 SPECFUN - Symbolic Special Functions : Fast and Certified Inria Saclay - Ile de France

Abstract : This paper reports on a six-year collaborative effort that cul- minated 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.

Autor: Georges Gonthier - Andrea Asperti - Jeremy Avigad - Yves Bertot - Cyril Cohen - François Garillot - Stéphane Le Roux - Assia Ma

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados