If you want to have a look into the state of the art of axiomatic systems that can be (and have been) used for proofs that can be checked by a computer, it sure

If you want to have a look into the state of the art of axiomatic systems that can be (and have been) used for proofs that can be checked by a computer, it surely is not a bad idea to read the Homotopy Type Theory (HoTT) book, which is freely available at > https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ If you prefer a more "established" way: Common systems for computer-checked proofs are Isabelle/HOL, Coq and Agda (the latter is often commonly "only" called a programming language, but also has been used for this purpose). For Isabelle/HOL (https://isabelle.in.tum.de/ https://isabelle.in.tum.de/) I only know the official documentation as a resource: https://isabelle.in.tum.de/documentation.html https://isabelle.in.tum.de/documentation.html For Coq (https://coq.inria.fr/ https://coq.inria.fr/) a good book book is "Coq'Art: The Calculus of Inductive Constructions" by Yves Bertot and Pierre Castéran. Unluckily it is not (legally) freely available. Finally for Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php) I recommend reading Ulf Norell's PhD thesis "Towards a practical programming language based on dependent type theory" and the more introductory paper "Dependently Typed Programming in Agda". Both texts are available at http://www.cse.chalmers.se/~ulfn/ http://www.cse.chalmers.se/~ulfn/