From the Universality of Mathematical Truth to the Interoperability of Proof Systems
Gilles Dowek · Lecture notes in computer science · 2022
Abstract The development of computerized proof systems, such as Coq, Matita, Agda, Lean, HOL 4, HOL Light, Isabelle/HOL, Mizar, etc. is a major step forward in the never ending quest of mathematical rigor.