1. Martin Aigner & Günter M. Ziegler (2018): Proofs from THE BOOK, 6th edition. Springer, doi:10.1007/978-3-662-57265-8.
  2. Ariane Alves Almeida, Ana Cristina Rocha-Oliveira, Thiago Mendonça Ferreira Ramos, Flávio Leonardo C. de Moura & Mauricio Ayala-Rincón (2019): The Computational Relevance of Formal Logic Through Formal Proofs. In: Proceedings 3rd Formal Methods Teaching FMTea, LNCS 11758. Springer, pp. 81–96, doi:10.1007/978-3-030-32441-4_6.
  3. Jesús Aransay, Clemens Ballarin, Martin Baillon, Paulo Emílio de Vilhena, Stephan Hohe, Florian Kammüller & Lawrence C. Paulson (2019): The Isabelle/HOL Algebra Library. Technical Report. Isabelle Library, University of Cambridge Computer Laboratory and Technische Universität München. Available at
  4. Mauricio Ayala-Rincón & Flávio Leonardo C. de Moura (2017): Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs. UTiCS. Springer, doi:10.1007/978-3-319-51653-0.
  5. Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter & Hendrik Spohr (2008): CERES: An analysis of Fürstenberg's proof of the infinity of primes. Theor. Comput. Sci. 403(2-3), pp. 160–175, doi:10.1016/j.tcs.2008.02.043.
  6. Jonas Bayer, Marco David, Abhik Pal & Benedikt Stock (2019): Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle, pp. 16–27, doi:10.1007/978-3-030-23250-4_2.
  7. Sandrine Blazy (2019): Teaching Deductive Verification in Why3 to Undergraduate Students. In: Proceedings 3rd Formal Methods Teaching FMTea, LNCS 11758. Springer, pp. 52–66, doi:10.1007/978-3-030-32441-4_4.
  8. Ricky Butler & David Lester (2007): A PVS Theory for Abstract Algebra. Available at Accessed in June 17, 2020.
  9. Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg & Vincent Siles (2016): Formalized linear algebra over Elementary Divisor Rings in Coq. Logical Methods in Computer Science 12(2:7), pp. 1–23, doi:10.2168/LMCS-12(2:7)2016.
  10. Cyril Cohen & Assia Mahboubi (2012): Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods in Computer Science 8(1:2), pp. 1–40, doi:10.2168/LMCS-8(1:2)2012.
  11. Catherine Dubois, Virgile Prevosto & Guillaume Burel (2019): Teaching Formal Methods to Future Engineers. In: Proceedings 3rd Formal Methods Teaching FMTea, LNCS 11758. Springer, pp. 69–80, doi:10.1007/978-3-030-32441-4_5.
  12. Manuel Eberl (2020): Fürstenberg's topology and his proof of the infinitude of primes. Arch. Formal Proofs 2020. Available at
  13. John B. Fraleigh (2002): A First Course in Abstract Algebra, 7th edition. Pearson.
  14. Hillel Fürstenberg (1955): On the Infinitude of Primes. Amer. Math, Monthly 62(5), pp. 353, doi:10.2307/2307043.
  15. André Luiz Galdino (2011): A PVS Theory for Groups. Available at Accessed in June 17, 2020.
  16. Herman Geuvers, Randy Pollack, Freek Wiedijk & Jan Zwanenburg (2002): A Constructive Algebraic Hierarchy in Coq. Journal of Symbolic Computation 34(4), pp. 271–286, doi:10.1006/jsco.2002.0552.
  17. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi & Laurent Théry (2013): A Machine-Checked Proof of the Odd Order Theorem. In: 4th International Conference on Interactive Theorem Proving ITP, LNCS 7998. Springer, pp. 163–179, doi:10.1007/978-3-642-39634-2_14.
  18. Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi & Laurent Théry (2007): A Modular Formalisation of Finite Group Theory. In: 20th International Conference Theorem Proving in Higher Order Logics TPHOLs, LNCS 4732. Springer, pp. 86–101, doi:10.1007/978-3-540-74591-4_8.
  19. John Harrison (2011): A formal proof of Pick's Theorem. Math. Struct. Comput. Sci. 21(4), pp. 715–729, doi:10.1017/S0960129511000089.
  20. Jónathan Heras, Francisco Jesús Martín-Mateos & Vico Pascual (2015): Modelling algebraic structures and morphisms in ACL2. Applicable Algebra in Engineering, Communication and Computing 26(3), pp. 277–303, doi:10.1007/s00200-015-0252-9.
  21. Israel (Yitzchak) Nathan Herstein (1975): Topics in algebra, 2nd edition. John Wiley & Sons.
  22. Thomas W. Hungerford (1980): Algebra. Graduate Texts in Mathematics 73. Springer, doi:10.1007/978-1-4612-6101-8. Reprint of the 1974 original.
  23. Paul Bernard Jackson (1995): Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Cornell University.
  24. Artur Kornilowicz & Christoph Schwarzweller (2014): The First Isomorphism Theorem and Other Properties of Rings. Formalized Mathematics 22(4), pp. 291– 301, doi:10.2478/forma-2014-0029.
  25. Thaynara Arielly de Lima, André Luiz Galdino, Andréia B. Avelar & Mauricio Ayala-Rincón (2020): Formalization of Ring Theory in PVS - Isomorphism Theorems, Principal, Prime and Maximal Ideals,Chinese Remainder Theorem. Available at
  26. Jade Philipoom (2018): Correct-by-Construction Finite Field Arithmetic in Coq. Master of Engineering in Computer Science, MIT.
  27. Kristin Yvonne Rozier (2019): On Teaching Applied Formal Methods in Aerospace Engineering. In: Proceedings 3rd Formal Methods Teaching FMTea, LNCS 11758. Springer, pp. 111–131, doi:10.1007/978-3-030-32441-4_8.
  28. Christoph Schwarzweller (2003): The Binomial Theorem for Algebraic Structures. Journal of Formalized Mathematics 12(3), pp. 559–564. Available at
  29. Andréia B. Avelar da Silva, Thaynara Arielly de Lima & André Luiz Galdino (2018): Formalizing Ring Theory in PVS. In: 9th International Conference on Interactive Theorem Proving ITP, LNCS 10895. Springer, pp. 40–47, doi:10.1007/978-3-319-94821-8_3.

Comments and questions to:
For website issues: