Irrationality and transcendence criteria for infinite series in Isabelle/HOL. (English) Zbl 1518.11003
The name “Isabelle” in the title of the paper under review is a proof assistant (interactive theorem prover). It was developed in by 1980s by Paulson and Nipkow. The abbreviation “HOL” refers to a higher-order logic formalism supported by Isabelle. The authors give a formalization of several well-known theorems and compare the proofs obtained using Isabelle/HOL with the known proofs.
Reviewer: Alexandra Shlapentokh (Greenville)
MSC:
| 11-04 | Software, source code, etc. for problems pertaining to number theory |
| 11J81 | Transcendence (general theory) |
| 11J68 | Approximation to algebraic numbers |
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 03B35 | Mechanization of proofs and logical operations |
| 68V35 | Digital mathematics libraries and repositories |
Software:
Archive Formal Proofs; kepler98; Irrationality_J_Hancl; Transcendence_Series_Hancl_Rucki; Irrational_Series_Erdos_Straus; Automath; Isabelle/HOLReferences:
| [1] | Bak, J.; Newman, D. J., Complex Analysis (2010), Springer · Zbl 1205.30001 |
| [2] | Blanchette, J. C.; Kaliszyk, C.; Paulson, L. C.; Urban, C., Hammering towards QED, J. Formaliz. Reason, 9, 1, 101-148 (2016) · Zbl 1451.68318 |
| [3] | Bordg, A.; Paulson, C., L.; Li, W., Grothendieck’s Schemes in Algebraic Geometry (2021), Archive of Formal Proofs |
| [4] | Bordg, A., Paulson, C., L. and Li, W. (2021). Simple Type Theory is not too Simple: Grothendieck’s Schemes without Dependent Types, arXiv:2104.09366. |
| [5] | Boyer, R.; Bundy, A., Automated Deduction - CADE 12, LNAI, 814, The QED Manifesto, 238-251 (1994), Springer-Verlag |
| [6] | Buzzard, K.; Commelin, J.; Massot, P., Formalising perfectoid spaces, arXiv:1910.12320, 299-312 |
| [7] | Dahmen, S. R.; Hölzl, J.; Lewis, R. Y., Formalizing the Solution to the Cap Set Problem, arXiv:1907.01449v1, Proceedings of Interactive Theorem Proving (ITP) (2019) |
| [8] | Eberl, M., Verified real asymptotics in Isabelle/HOL, Proceedings of International Symposium on Symbolic and Algebraic Computation (2019) · Zbl 1467.68204 · doi:10.1145/3326229.3326240 |
| [9] | Eberl, M., Elementary Facts About the Distribution of Primes, Archive of Formal Proofs (2019), formal proof development |
| [10] | Eberl, M.; Paulson, L. C., The Prime Number Theorem, Archive of Formal Proofs (2018), formal proof development |
| [11] | Erdős, P., Sur certaines series à valeur irrationelle, Enseignment Math, 4, 93-100 (1958) · Zbl 0080.03305 |
| [12] | Erdős, P., Some problems and results on the irrationality of the sum of infinite series, J. Math. Sci, 10, 1-7 (1975) · Zbl 0372.10023 |
| [13] | Erdős, P.; Straus, E. G., On the irrationality of certain series, Pacific J. Math., 55, 1, 85-92 (1974) · Zbl 0279.10026 · doi:10.2140/pjm.1974.55.85 |
| [14] | Erdős, P.; Straus, E. G., Some number theoretic results, Pacific J. Math., 36, 635-646 (1971) · Zbl 0216.32201 · doi:10.2140/pjm.1971.36.635 |
| [15] | Gonthier, G., Formal proof-the four-color theorem, Not. Am. Math. Soc, 55, 11, 1382-1393 (2008) · Zbl 1195.05026 |
| [16] | Gouëzel, S.; Shchur, V., A corrected quantitative version of the Morse lemma, J. Funct. Anal, 277, 4, 1258-1268 (2019) · Zbl 1419.53049 |
| [17] | Gowers, W. T.; Alon, N.; Bourgain, J.; Connes, A.; Gromov, M.; Milman, V., Visions in Mathematics. Modern Birkhäuser Classics, Rough structure and classification, 79-117 (2010), Birkhäuser Basel |
| [18] | Hales, T. C., A proof of the Kepler conjecture, Ann. Math., 162, 3, 1065-1185 (2005) · Zbl 1096.52010 · doi:10.4007/annals.2005.162.1065 |
| [19] | Hales, T.; Adams, M.; Bauer, G.; Dang, T. D.; Harrison, J.; Hoang, L. T.; Kaliszyk, C.; Magron, V.; McLaughlin, S.; Nguyen, T. T.; Nguyen, Q. T.; Nipkow, T.; Obua, S.; Pleso, J.; Rute, J.; Solovyev, A.; Ta, T. H. A.; Tran, N. T.; Trieu, T. D.; Urban, J.; Vu, K.; Zumkeller, R., A formal proof of the Kepler conjecture, Forum Math. Pi, 5, E2 (2017) · Zbl 1379.52018 |
| [20] | Hančl, J., Criterion for irrational sequences, J. Number Theory, 43, 1, 88-92 (1993) · Zbl 0768.11021 |
| [21] | Hančl, J., Transcendental sequences, Math. Slov, 46, 177-179 (1996) · Zbl 0888.11029 |
| [22] | Hančl, J., Two criteria for transcendental sequences, Le Matematiche, 56, 149-160 (2001) · Zbl 1173.11338 |
| [23] | Hančl, J., Irrational rapidly convergent series, Rend. Sem. Mat. Univ. Padova, 107, 225-231 (2002) · Zbl 1165.40301 |
| [24] | Hančl, J.; Rucki, P., The transcendence of certain infinite series, Rocky Mountain J. Math., 35, 2, 531-537 (2005) · Zbl 1092.11033 · doi:10.1216/rmjm/1181069744 |
| [25] | Hölzl, J.; Immler, F.; Huffman, B., International Conference on Interactive Theorem Proving, Type classes and filters for mathematical analysis in Isabelle/HOL, 279-294 (2013), Berlin, Heidelberg: Springer, Berlin, Heidelberg · Zbl 1317.68213 |
| [26] | van Benthem, L. S., Checking Landau’s “Grundlagen” in the AUTOMATH system (1977), Eindhoven University of Technology · Zbl 0402.68064 · doi:10.6100/IR23183 |
| [27] | Koutsoukou-Argyraki, A., Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started, Jahresber. Dtsch. Math. Ver., 123, 3-26 (2021) · Zbl 1495.68241 · doi:10.1365/s13291-020-00221-1 |
| [28] | Koutsoukou-Argyraki, A.; Li, W., Irrational rapidly convergent series (2018), Archive of Formal Proofs |
| [29] | Koutsoukou-Argyraki, A.; Li, W., The transcendence of certain infinite series (2019), Archive of Formal Proofs |
| [30] | Koutsoukou-Argyraki, A.; Li, W., Irrationality Criteria for Series by Erdős and Straus (2020), Archive of Formal Proofs |
| [31] | Mahler, K., Lectures on Transcendental Numbers, Lecture Notes in Mathematics, 546 (1976), Springer-Verlag Berlin-Heidelberg-New York · Zbl 0213.32703 |
| [32] | Nipkow, T.; Paulson, L. C.; Wenzel, M., Lecture Notes in Computer Science, 2283, Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Springer-Verlag Berlin-Heidelberg · Zbl 0994.68131 |
| [33] | Nishioka, K., Mahler Functions and Transcendence, Lecture Notes in Mathematics 1631 (1996), Springer-Verlag Berlin-Heidelberg · Zbl 0876.11034 |
| [34] | Nyblom, M. A., A theorem on transcendence of infinite series, Rocky Mountain J. Math., 30, 1111-1120 (2000) · Zbl 0972.11063 · doi:10.1216/rmjm/1021477261 |
| [35] | Nyblom, M. A., A theorem on transcendence of infinite series II, J. Number Theory, 91, 71-80 (2001) · Zbl 1012.11063 · doi:10.1006/jnth.2001.2672 |
| [36] | Paulson, L. C., The foundation of a generic theorem prover, J. Autom. Reason, 5, 3, 363-397 (1989) · Zbl 0679.68173 |
| [37] | Paulson, L. C., ALEXANDRIA: Large-scale formal proof for the working mathematician, project description (122018) |
| [38] | Roth, K. F., Rational approximations to algebraic numbers, Mathematica, 1, 3, 1-20 (1955) · Zbl 0064.28501 · doi:10.1112/S0025579300000644 |
| [39] | Sándor, J., Some classes of irrational numbers, Studia Univ. Babeş-Bolyai Math, 29, 3-12 (1994) · Zbl 0544.10033 |
| [40] | Wiedijk, F., The De Bruijn Factor, Technical report, Nijmegen, Netherlands: Department of Computer Science Nijmegen University, Nijmegen, Netherlands |
| [41] | Wiedijk, F., The De Bruijn Factor (webpage) |
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.
