Prople
Jeremmy Avigad •
Kevin Buzzard •
François Chollet •
Georges Gonthier •
Timothy Gowers •
Thomas C. Hales •
Larry Paulson •
Christian Szegedy •
Josef Urban
Proof assistants
Isabelle •
Coq •
HOL Light •
Metamath •
Lean Community •
Mizar
Some articles on AI-assisted proofs
• A. Alemi, F. Chollet, G. Irving, C. Szegedy, J. Urban (2016)
DeepMath - Deep Sequence Models for Premise Selection, NIPS-30
• C. Kaliszyk, F. Chollet, C. Szegedy. (2017)
HolStep: a Machine Learning Dataset for Higher-Order Logic Theorem Proving, ICLR-5.
• S. Loos, G. Irving, C. Szegedy, C. Kaliszyk. (2017)
Deep Network Guided Proof Search. LPAR-21. pp. 85-105
• K. Bansal et al. (2019)
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving, ICML-36.
• A. Paliwal et al. (2020)
Graph Representations for Higher-Order Logic and Theorem Proving AAAI-2020.
Some computer-assisted proofs
Four Color Theorem
•
The problem and its history (Wikipedia)
• Appel, Kenneth; Haken, Wolfgang (1977), Every Planar Map is Four Colorable. I. Discharging, Illinois J. of Math., 21 (3): 429–490.
• Appel, Kenneth; Haken, Wolfgang; Koch, John (1977), Every Planar Map is Four Colorable. II. Reducibility, Illinois J. of Math., 21 (3): 491–567.
• Robertson, Neil; Sanders, Daniel P.; Seymour, Paul; Thomas, Robin (1996),
A New Proof of the Four-Colour Theorem,
Electronic Research Announcements of The AMS. This proof
is also computer-assisted and similar to but simpler than Appel and Haken's proof.
• Gonthier, Georges (2008),
Formal Proof—The Four-Color Theorem,
Notices of the AMS, 55 (11): 1382–1393. This proof used Coq as proof-assistant.
The Kepler Conjecture
•
The problem and its history (Wikipedia)
• Hales, Thomas C. (2005),
A proof of the Kepler conjecture, Annals of Mathematics, Second Series, 162 (3): 1065–1185.
• Hales, Thomas C. and 21 other co-authors (2017),
A formal proof of the Kepler Conjecture, Arxiv. This proof used Isabelle and HOL Light as proof-assistants.
Non-existence of a Finite Projective Plane of order 10
•
The problem and its history (Wikipedia)
• Lam, Clement W. H. (1991).
The Search for a Finite Projective Plane of order 10. The American Mathematical Monthly. 98 (4): 305–318.
• Bright, C. et al. (2021).
A SAT-based Resolution of Lam's Problem, AAAI-2021.
Robbins Conjecture
•
The problem and its history (Wikipedia)
• S. Winker.
Absorption and idempotency criteria for a problem in near-Boolean algebras. Journal of Algebra, 153:414–423, 1992.
• Mann, Allen (2003).
A Complete Proof of the Robinns Conjecture. M. A. Thesis Excerpt
Ramsey's Theorem and Exact values of Ramsey numbers
•
The problem and its history (Wikipedia)
• Radziszowski, Stanisław P. (1994 - 2017)
Small Ramsey Numbers. Electronic Journal of Combinatorics, Dynamic Syrveys.
Van der Waerden's Theorem and Exact values of van der Waerden numbers
•
The theorem and its history (Wikipedia)
• See the Wikipedia entry
Van der Waerden Number for values and bounds.