Computer Assisted Proof is closely aligned with my primary research focus in Computer Science. My work bridges the fields of mathematics and computer science, utilizing advanced computational techniques to explore and validate mathematical theorems.
The emergence of automated and semi-automated proof systems has transformed the way we approach mathematical problems. By integrating formal logic, combinatorics, and computational methods, we can tackle conjectures and problems that were previously out of reach. My research emphasizes Formal Verification that ensures the correctness of mathematical proofs and computational algorithms; and
Experimental Mathematics that uses computation to uncover patterns, explore conjectures, and propose new theorems. This page serves as a curated resource for tools, techniques, and systems that contribute to this exciting area of study.
SAT / SMT
SAT / SMT Researchers
Carlos Ansótegui
•
Clark Barrett
•
Christian Bessière
•
Jeremias Berg
• Olaf Beyersdorff
•
Armin Biere
•
Maria Paola Bonacina
•
Nikolaj Bjørner
•
Curtis Bright
•
Shaowei Cai
•
Supratik Chakraborty
•
Vašek Chvátal
•
Katalin Fazekas
•
Pascal Fontaine
•
John Franco
•
Vijay Ganesh
•
Holger Hoos
•
Marijn Heule
•
Warren A. Hunt Jr.
•
Alexey Ignatiev
•
Mikoláš Janota
•
Matti Järvisalo
•
Jie-Hong Roland Jiang
•
Matt Kaufmann
•
Benjamin Kiesl-Reiter
•
Antonina Kolokolova
•
Michal Kouril
•
Daniel Kroening
•
Oliver Kullmann
•
Daniel Le Berre
•
Jordi Levy
•
Inês Lynce
•
Meena Mahajan
•
Joao Marques-Silva
•
Ruben Martins
•
Kuldeep S. Meel
•
Stefan Mengel
•
J Strother Moore
•
Leonardo de Moura
•
Alexander Nadel
•
Nina Narodytska
•
Aina Niemetz
•
Jakob Nordström
•
Luca Pulina
•
Karem Sakallah
•
Laurent Simon
•
Roberto Sebastiani
•
Martina Seidl
•
Carsten Sinz
•
Ofer Strichman
•
Naoyuki Tamura
•
Xishun Zhao
SAT / SMT solvers
•
CaDiCaL: A simplified and modern SAT solver designed for research and industrial applications.
•
Clasp: A conflict-driven answer set solver for solving SAT problems and related logic programs.
•
CVC5: An advanced SMT solver with SAT-solving capabilities and support for theories like arithmetic and bit-vectors.
•
CryptoMiniSat: A SAT solver optimized for cryptographic applications with advanced debugging tools.
•
Kissat: A high-performance SAT solver with scalability for industrial problems.
•
MapleSAT: A SAT solver that uses machine learning techniques to improve decision heuristics.
•
MiniSat: A lightweight and efficient SAT solver often used as a foundation for other solvers.
•
PicoSAT: A small and efficient SAT solver often used in teaching and experimentation.
•
PrecoSAT: A SAT solver designed to test experimental SAT-solving techniques.
•
RISS: A robust SAT solver with advanced preprocessing and inprocessing capabilities.
•
SAT4J: A Java-based SAT solver designed for embedding in Java applications.
•
SATCH: A minimalistic SAT solver for educational and research purposes.
•
Splatz: A SAT solver optimized for high scalability in industrial use cases.
•
YalSAT: A lightweight SAT solver using stochastic local search techniques.
•
Z3: A high-performance SMT and SAT solver developed by Microsoft Research for formal verification and symbolic reasoning.
Interactive Theorem Provers
ITP Researchers
Jeremmy Avigad •
Kevin Buzzard •
François Chollet •
Georges Gonthier •
Timothy Gowers •
Thomas C. Hales •
Larry Paulson •
Christian Szegedy •
Josef Urban
Proof Assistants
•
Coq: A proof assistant for developing machine-checked proofs, focusing on typed functional programming and formal verification.
•
HOL4: A theorem prover for higher-order logic, particularly useful in hardware and software verification.
•
HOL Light: A lightweight proof assistant for higher-order logic, known for its simplicity and focus on mathematical proofs.
•
Isabelle: A generic interactive theorem prover supporting multiple logical formalisms, including higher-order logic.
•
Lean: An interactive proof assistant and programming language widely used for formal mathematics and theorem proving.
•
NuPRL: A proof development system supporting constructive type theory for formal mathematics and verification.
•
Proof General: A generic Emacs-based environment for interacting with proof assistants like Coq, Isabelle, and Lean.
•
Mizar: A proof assistant designed for formalizing mathematical knowledge and creating a library of formalized mathematics.
•
SASyLF: A lightweight proof assistant designed for educational purposes and focusing on language theory and formal reasoning.
•
Why3: A platform for deductive program verification that integrates multiple proof assistants and SMT solvers.
Some articles on AI-assisted proofs
• S. Chakraborty et al. (2025)
Towards Neural Synthesis for SMT-assisted Proof-Oriented Programming,
ICSE, pp. 13-25.
• T. H. Trinh et al. (2024)
Solving olympiad geometry without human demonstrations, Nature, 625, pp. 476–482.
• J. Yao et al. (2023)
Leveraging Large Language Models for Automated Proof Synthesis in Rust.
• A. Paliwal et al. (2020)
Graph Representations for Higher-Order Logic and Theorem Proving, AAAI-2020.
• K. Bansal et al. (2019)
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving, ICML-36.
• S. Loos, G. Irving, C. Szegedy, C. Kaliszyk. (2017)
Deep Network Guided Proof Search. LPAR-21. pp. 85-105.
• C. Kaliszyk, F. Chollet, C. Szegedy. (2017)
HolStep: a Machine Learning Dataset for Higher-Order Logic Theorem Proving, ICLR-5.
• A. Alemi, F. Chollet, G. Irving, C. Szegedy, J. Urban (2016)
DeepMath - Deep Sequence Models for Premise Selection, NIPS-30.
Some computer-assisted proofs
Schur Number 5
•
The problem and its history (Wikipedia)
• Marijn Heule (2018).
Schur Number Five. Proceedings of the National Academy of Sciences. This proof used SAT solvers.
Pythagorean Triples Problem
•
The problem and its history (Wikipedia)
• Marijn Heule, Oliver Kullmann, and Victor Marek (2016).
Solving and Verifying the Boolean Pythagorean Triples Problem. Nature. This proof used SAT solvers and extensive computational resources.
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.