Formalization of the Lindemann-Weierstrass theorem. (English) Zbl 1483.68485
Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 65-80 (2017).
Summary: This article details a formalization in Coq of the Lindemann-Weierstrass theorem which gives a transcendence criterion for complex numbers: this theorem establishes a link between the linear independence of a set of algebraic numbers and the algebraic independence of the exponentials of these numbers. As we follow Baker’s proof, we discuss the difficulties of its formalization and explain how we resolved them in Coq. Most of these difficulties revolve around multivariate polynomials and their relationship with the conjugates of a univariate polynomial. Their study ultimately leads to alternative forms of the fundamental theorem of symmetric polynomials. This formalization uses mainly the Mathcomp library for the part relying on algebra, and the Coquelicot library and the Coq standard library of real numbers for the calculus part.
For the entire collection see [Zbl 1369.68009].
For the entire collection see [Zbl 1369.68009].
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 11J81 | Transcendence (general theory) |
Software:
CoqReferences:
| [1] | Formalization of the Lindemann-Weierstrass theorem in Coq. http://www-sop.inria.fr/marelle/lindemann/ |
| [2] | Baker, A., Transcendental Number Theory (1990), Cambridge: Cambridge University Press, Cambridge · Zbl 0715.11032 |
| [3] | Bernard, S., Bertot, Y., Rideau, L., Strub, P.Y.: Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 76-87. ACM (2016) |
| [4] | Bingham, J., Formalizing a proof that e is transcendental, J. Formaliz. Reason., 4, 1, 71-84 (2011) · Zbl 1451.68317 |
| [5] | Boldo, S.; Lelay, C.; Melquiond, G., Coquelicot: a user-friendly library of real analysis for Coq, Math. Comput. Sci., 9, 1, 41-62 (2015) · Zbl 1322.68176 · doi:10.1007/s11786-014-0181-1 |
| [6] | Cohen, C.: Finmap library. http://github.com/math-comp/finmap |
| [7] | Cohen, C.: Formalized algebraic numbers: construction and first-order theory. Ph.D. thesis, Citeseer (2013) |
| [8] | Coq development team: the Coq proof assistant (2008). http://coq.inria.fr |
| [9] | Gonthier, G., Formal proof – the four-color theorem, Not. AMS, 55, 11, 1382-1393 (2008) · Zbl 1195.05026 |
| [10] | Gonthier, G.; Blazy, S.; Paulin-Mohring, C.; Pichardie, D., A machine-checked proof of the odd order theorem, Interactive Theorem Proving, 163-179 (2013), Heidelberg: Springer, Heidelberg · Zbl 1317.68211 · doi:10.1007/978-3-642-39634-2_14 |
| [11] | Hermite, C.: Sur la fonction exponentielle. In: Comptes-Rendus de l’Académie des Sciences, vol. 77, pp. 18-24, 74-79, 226-233, 285-293. Paris (1873) · JFM 05.0248.01 |
| [12] | Lang, S., Algebra (2002), New York: Springer, New York · Zbl 0984.00001 · doi:10.1007/978-1-4613-0041-0 |
| [13] | Lindemann, F., Über die zahl \(\pi \), Math. Ann., 20, 2, 213-225 (1882) · JFM 14.0369.04 · doi:10.1007/BF01446522 |
| [14] | Liouville, J., Sur des classes très-étendues de quantités dont la valeur n’est ni algébrique, ni même réductible à des irrationnelles algébriques, J. de mathématiques pures et appliquées, 16, 133-142 (1851) |
| [15] | Muñoz, C.; Narkawicz, A., Formalization of a representation of Bernstein polynomials and applications to global optimization, J. Autom. Reason., 51, 2, 151-196 (2013) · Zbl 1314.68286 · doi:10.1007/s10817-012-9256-3 |
| [16] | Weierstrass, K.: Zu Lindemann’s Abhandlung: “Über die Ludolph’sche Zahl.”. Akademie der Wissenschaften (1885) · JFM 17.0414.01 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
