Skip to Main content Skip to Navigation

Formalized algebraic numbers: construction and first-order theory.

Abstract : This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in proof assistants, Coq in our case: the intuitionistic construction of real algebraic numbers together with the proof they form a real closed field, and the programming and certification of quantifier elimination procedures for the theories of algebraically closed fields and real closed fields. In order to reach those results, we brought multiple contributions to the toolboxes and formalization and proof methodologies in Coq. More particularly, we provide in Coq/SSReflect a framework to work with quotient types. We provide a complete library about ordered and normed number algebraic structures. We wrote a short implementation of Cauchy reals together with tactics to deal easily with reasoning using assertions of the form "let n be a big enough number", commonly used in mathematical paper proofs. We also developed a short library of real polynomial analysis. A big part of our contributions is useful for the formalization of the proof of Odd Order Theorem and they also aim at helping to prove and certify more efficient quantifier elimination procedures on reals.
Complete list of metadata

Cited literature [86 references]  Display  Hide  Download
Contributor : Cyril Cohen <>
Submitted on : Thursday, January 24, 2013 - 3:30:41 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on: : Saturday, April 1, 2017 - 9:46:21 AM



  • HAL Id : pastel-00780446, version 1



Cyril Cohen. Formalized algebraic numbers: construction and first-order theory.. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English. ⟨pastel-00780446⟩



Record views


Files downloads