Automatic theorem proving for mathematicians
A webibliography (in progress)
Automatic theorem provers are computer programs that can assert the validity of a mathematical proof, help to build mathematical proofs, and can even prove some proofs themselves. They recently had great success by allowing to certify proofs of the 4-colour theorem and the Feit-Thompson theorem (Gonthier and his collaborators) or Hales’s proof of the Kepler conjecture (Hales himself). Even more recently, a team around Kevin Buzzard embarked in computer-checking Scholze’s theory of perfectoid spaces.
Which theorem prover to chose ?
A description of some of them by Thomas Hales, ▻https://jiggerwit.wordpress.com/2018/04/14/the-architecture-of-proof-assistants
Lean
A review of the Lean theorem prover, by Thomas Hales, ▻https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover
Theorem proving in Lean, ▻https://leanprover.github.io/theorem_proving_in_lean
Coq
Winter school on Coq and Mathematical components, ▻https://team.inria.fr/marelle/en/coq-winter-school-2018-2019-ssreflect-mathcomp
A book on Mathematical components, by Assia Mahboubi and Enrico Tassi, ▻https://math-comp.github.io/mcb