GNN-SMT
A Consortium Based Proof Automation for Lean 4
The Project
Stanford Centaur Lab takes a two-pronged approach to proof automation in Lean 4: Lean-SMT and a general theorem proving agent. Lean-SMT integrates SMT (Satisfiability Modulo Theory) solvers to extend Lean's capabilities and offer a new proving tactic. The general theorem proving agent takes inspiration from how real mathematicians conduct mathematics, and uses Machine-Learning assisted Monte-Carlo Tree Search (the technique behind AI breakthroughs such as AlphaGo) to explore a large space of proof states based on a heuristic process.
The Team
Clark Barrett is a Professor (Research) of Computer Science at Stanford University. His expertise is in automated reasoning and its applications. He was an early pioneer in satisfiability modulo theories and formal hardware verification. More recently, he has also pioneered techniques for applying formal methods to AI systems. He is the director of the Stanford Center for Automated Reasoning (Centaur) and co-director of the Stanford Center for AI Safety. He is an ACM Fellow and two-time winner of the Computer Aided Verification (CAV) award.
Leni Aniva is a CS Ph.D. student at Stanford University. She is the main author of the tool Pantograph, which is used by a wide array of machine-assisted theorem proving projects in academia and industry. She has years of software engineering experience, and has worked on SMT solvers, proof assistants, and machine learning agents, with an emphasis on diagnosability and efficiency.
Abdalrhman Mohamed is a Ph.D. candidate at Stanford University, working at the intersection of theorem proving and model checking. He is a core developer of cvc5 and of Lean-SMT, a tactic that integrates cvc5 into Lean. His research focuses on SMT solving and its applications in formal verification.
Harun Khan is a Ph.D. student in Computer Science at Stanford University. His research focuses on formal verification, theorem proving, and automated reasoning. He has worked on mathematical formalizations in the Lean Theorem Prover, including Robust Mean Estimation by All Means, and on formalizing proof rules to enable the integration of SMT solvers with Lean.