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.v in a subfolder under UniMath/UniMath, and had to Require Export UniMath.Foundations.Propositions. at the top. Also, I had to place etags in the PATH.
• Lean
  • Lean for the Curious Mathematician ‘20
    • Mathematics in Lean introduction - Patrick Massot
  • 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
  • Comparison of Two Theorem Provers: Isabelle/HOL and Coq
  • Isabelle Theorem Prover tutorial
• 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 univalent at ias.edu
• C. Szegedy
  • Formal Reasoning, Program Synthesis (2021)
  • Scale.ai interview with 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)

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
  • Talks

Summer Schools

• School on Univalent Mathematics ‘22, ‘19

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

• HOList

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
  • Blog
    • Formalism, Platonism and Mentalese (2017)
  • MathZero, the Classification Problem, and Set-Theoretic Type Theory (2020)

Other

• Computation Theory
• Engineering Math
• Philosophy of Math