References
- Bak, J., and Newman, D. J. (2010). Complex Analysis, 3rd ed. Springer.
- Blanchette, J. C., Kaliszyk, C., Paulson, L. C., Urban, C. (2016). Hammering towards QED. J. Formaliz. Reason. 9(1): 101–148.
- Bordg, A., Paulson C., L. and Li, W., Grothendieck’s Schemes in Algebraic Geometry, Archive of Formal Proofs (2021), formal proof development, Available at: https://isa-afp.org/entries/Grothendieck_Schemes.html.
- 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.
- Boyer, R. et al., (1994). The QED Manifesto. In Bundy, A., ed. Automated Deduction – CADE 12, LNAI 814, Springer-Verlag; pp. 238–251.
- Buzzard, K., Commelin, J., Massot, P. Formalising perfectoid spaces, arXiv:1910.12320, in CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 299–312.
- Dahmen, S. R., Hölzl, J., Lewis, R. Y. (2019). Formalizing the Solution to the Cap Set Problem, arXiv:1907.01449v1, Proceedings of Interactive Theorem Proving (ITP). https://drops.dagstuhl.de/opus/volltexte.
- Eberl, M. (2019). Verified real asymptotics in Isabelle/HOL. In Proceedings of International Symposium on Symbolic and Algebraic Computation. . doi:https://doi.org/10.1145/3326229.3326240
- Eberl, M. Elementary Facts About the Distribution of Primes, Archive of Formal Proofs (2019), formal proof development. Available at: https://www.isa-afp.org/entries/Prime_Distribution_Elementary.html.
- Eberl, M., Paulson, L.C. The Prime Number Theorem, Archive of Formal Proofs (2018), formal proof development. Available at: https://www.isa-afp.org/entries/Prime_Number_Theorem.html.
- Erdős, P. (1958). Sur certaines series à valeur irrationelle. Enseignment Math. 4: 93–100.
- Erdős, P. (1975). Some problems and results on the irrationality of the sum of infinite series. J. Math. Sci. 10: 1–7.
- Erdős, P., Straus, E. G. (1974). On the irrationality of certain series. Pacific J. Math. 55(1): 85–92. doi:https://doi.org/10.2140/pjm.1974.55.85
- Erdős, P., Straus, E. G. (1971). Some number theoretic results. Pacific J. Math. 36: 635–646. doi:https://doi.org/10.2140/pjm.1971.36.635
- Gonthier, G. (2008). Formal proof–the four-color theorem. Not. Am. Math. Soc. 55(11): 1382–1393.
- Gouëzel, S., Shchur, V. (2019). A corrected quantitative version of the Morse lemma. J. Funct. Anal. 277(4): 1258–1268.
- Gowers, W. T. (2010). Rough structure and classification. In: Alon N., Bourgain J., Connes A., Gromov M., Milman V., eds. Visions in Mathematics. Modern Birkhäuser Classics. Birkhäuser Basel. pp. 79–117.
- Hales, T. C. (2005). A proof of the Kepler conjecture. Ann. Math. 162 (3): 1065–1185. doi:https://doi.org/10.4007/annals.2005.162.1065
- 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. (2017). A formal proof of the Kepler conjecture. Forum Math. Pi, 5, E2.
- Hančl, J. (1993). Criterion for irrational sequences. J. Number Theory. 43(1): 88–92.
- Hančl, J. (1996). Transcendental sequences. Math. Slov. 46, 177–179.
- Hančl, J. (2001). Two criteria for transcendental sequences, Le Matematiche, 56: 149–160.
- Hančl, J. (2002). Irrational rapidly convergent series. Rend. Sem. Mat. Univ. Padova 107, 225–231.
- Hančl, J., Rucki, P. (2005), The transcendence of certain infinite series. Rocky Mountain J. Math. 35(2): 531–537. doi:https://doi.org/10.1216/rmjm/1181069744
- Hölzl, J., Immler, F. and Huffman, B. Type classes and filters for mathematical analysis in Isabelle/HOL. In International Conference on Interactive Theorem Proving 2013 Jul 22. Berlin, Heidelberg: Springer; pp. 279–294.
- Jutting, L.S. van Benthem. Checking Landau’s “Grundlagen” in the AUTOMATH system. PhD thesis, Eindhoven University of Technology (1977). https://doi.org/10.6100/IR23183.
- 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, pp. 3–26(2021). doi:https://doi.org/10.1365/s13291-020-00221-1.
- Koutsoukou-Argyraki, A., Li, W., Irrational rapidly convergent series, Archive of Formal Proofs (2018), formal proof development. Available at: https://www.isa-afp.org/entries/Irrationality_J_Hancl.html.
- Koutsoukou-Argyraki, A., Li, W., The transcendence of certain infinite series, Archive of Formal Proofs (2019), formal proof development, Available at: https://www.isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html.
- Koutsoukou-Argyraki, A., Li, W., Irrationality Criteria for Series by Erdős and Straus, Archive of Formal Proofs (2020), formal proof development. Available at: https://www.isa-afp.org/entries/Irrational_Series_Erdos_Straus.html.
- Mahler, K. (1976). Lectures on Transcendental Numbers, Lecture Notes in Mathematics, Vol. 546, Springer-Verlag Berlin-Heidelberg-New York.
- Nipkow, T., Paulson, L. C., Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, Vol. 2283, Springer-Verlag Berlin-Heidelberg.
- Nishioka, K. (1996). Mahler Functions and Transcendence, Lecture Notes in Mathematics 1631, Springer-Verlag Berlin-Heidelberg.
- Nyblom, M.A. (2000). A theorem on transcendence of infinite series. Rocky Mountain J. Math. 30: 1111–1120. doi:https://doi.org/10.1216/rmjm/1021477261
- Nyblom, M. A. (2001). A theorem on transcendence of infinite series II. J. Number Theory. 91: 71–80. doi:https://doi.org/10.1006/jnth.2001.2672
- Paulson, L. C. (1989). The foundation of a generic theorem prover, J. Autom. Reason. 5(3): 363–397, Kluwer Academic Publishers.
- Paulson, L. C., ALEXANDRIA: Large-scale formal proof for the working mathematician, project description, (12 Nov. 2018). Available at: http://www.cl.cam.ac.uk/lp15/Grants/Alexandria/.
- Roth, K. F. (1955). Rational approximations to algebraic numbers. Mathematica 2, Part 1(3): 1–20. doi:https://doi.org/10.1112/S0025579300000644
- Sándor, J. (1994). Some classes of irrational numbers. Studia Univ. Babeş-Bolyai Math., 29: 3–12.
- Wiedijk, F., The De Bruijn Factor, Technical report. Nijmegen, Netherlands: Department of Computer Science Nijmegen University. Available at: https://www.cs.ru.nl/freek/factor/factor.pdf.
- Wiedijk, F. The De Bruijn Factor (webpage). Available at: http://www.cs.ru.nl/freek/factor/.