Automated Theorem Proving
Books
- Homotopy Type Theory - Univalent Foundations of Mathematics
- Egbert Rijke: Introduction to Homotopy Type Theory (2022)
Languages
- Coq
- Coq in a hurry, Yves Bertot (2017)
- Spartan Martin-Löf Type Theory, Andrej Bauer (2019)
- Video
- How to use Coq with Proof General, Andrej Bauer (2011). I installed UniMath Coq on MacBook, had to create
pierce_lem.vin a subfolder underUniMath/UniMath, and had toRequire Export UniMath.Foundations.Propositions.at the top. Also, I had to placeetagsin thePATH.
- How to use Coq with Proof General, Andrej Bauer (2011). I installed UniMath Coq on MacBook, had to create
- Lean
- Lean for the Curious Mathematician ‘20
- Leonardo de Moura & Sebastian Ullrich: The Lean 4 Theorem Prover and Programming Language (2021)
- Metamath, by Norman Megill, revised by David A. Wheeler (2019)
- HOL Light
- Isabelle
- Homotopy Type Theory Code: COQ and AGDA
- AGDA wiki
Posts
- Building the Mathematical Library of the Future, Kevin Hartnett (2020)
- Julie Rehmeyer: Voevodsky’s Mathematical Revolution (2013)
- Peter Woit: Interview(s) with Vladimir Voevodsky (2012)
- How Close Are Computers to Automating Mathematical Reasoning?, S. Ornes (2020)
- OpenAI Proof Assistant for Metamath (2020)
- Jeremy Avigad: Mathematics and the formal turn (2023)
- OpenAI: Hunter Lightman et al: Improving mathematical reasoning with process supervision (2023), paper, Stanislas Polu Tweet
Talks
- V. Voevodsky
- UniMath, Heidelberg (2016), slides
- Univalent Foundations: New Foundations of Mathematics, IAS Faculty Lecture (2014), outline
- Foundations of Mathematics and Homotopy Theory, (2006), see links in the description
- Search
univalentat ias.edu
- C. Szegedy
- Adam Pease: How (and why) to Build and Automated Theorem Prover: De-mystifying Logical Inference (2021)
Papers
- Robert Harper
- Anders Mortberg: Synthetic Cohomology Theory in Cubical Agda (2023)
- Nature: Mathematical discoveries from program search with large language models B Romera-Pardes et al (2023)
Seminars
- Harvard CMSA: New Technologies in Mathematics
- Yuhai Wu: Memorizing Transformers (2022)
- Stanislas Polu: Formal Mathematics: Statement Curriculum Learning (2022)
- HoTTTest Summer School 2022
- HoTT 2023
Summer Schools
Articles
- Mathematical Reasoning via Self-supervised Skip-tree Training, M.N. Rabe et al, Google Research (2021)
- Learning to Reason in Large Theories without Imitation, K. Bansal, C. Szegedy et al, Google Research (2021)
- G. Lample et al: HyperTree Proof Search for Neural Theorem Proving (2022)
- A. Jiang et al: Draft, Sketch and Prove: Guiding Formal Theorem Provers With Informal Proofs (2022)
- S. Polu, I. Sutskever: Generative Language Modeling for Automated Theorem Proving (2020)
- Y. Wu, C. Szegedy et al: Autoformalization with Large Language Models (2022)
- M Chen, I. Sutskever, W. Zaremba et al: Evaluating Large Language Models Trained on Code (2021)
- X. Zhao et al: Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving (2023)
- S. Polu et al: Formal Mathematics Statement Curriculum Learning (2022)
- K. Zheng et al: MiniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics (2022)
Software Verification
- V. D’Silva et al: A Survey of Automated Techniques for Formal Software Verification (2008)
Benchmarks
People
- Thierry Coquand
- Christian Szegedy
- Vladimir Voevodsky (1966-2017)
- Yuhuai(Tony) Wu
- Stanislas Polu
- Jeremy Avigad
- Mathematical Logic and Computation (2022, 2nd ed)
- David McAllester