A Principled Approach to Proof Search with Applications to Siderenko’s Conjecture

The Project

This project proposes new proof methods to automate and streamline the proof discovery process for significant unsolved problems. To this end, this work seeks to establish a rigorous theoretical framework, planted proofs, and develop novel algorithms to efficiently and scalability derive proofs for open problems. As a proof-of-concept, this project will focus on creating a theoretically sound method for finding resolution proofs for satisfiability (SAT) formulas and developing machine learning tools to address Siderenko’s conjecture, a key open problem in combinatorics. By bridging these gaps, the project holds the potential to advance both theoretical and practical aspects of AI in mathematics.

The Team

Pravesh K Kothari is an Assistant Professor in the Computer Science Department at Princeton University. Earlier, he was an Assistant Professor in the Computer Science Department at Carnegie Mellon University and a Research Instructor of Computer Science jointly hosted by the Institute for Advanced Study, Princeton, and the Department of Computer Science at Princeton University from 2016-19. Dr. Kothari's research interests span several topics in theoretical computer science such as convex optimization and applications to algorithm design, algorithms and lower bounds for statistical estimation and average-case combinatorial optimization, and spectral methods and connections to random matrix theory, coding theory and extremal combinatorics. Dr Kothari is a recipient of the Presburger Award (2024), IIT Kanpur Young Alumnus Award (2023), Sloan Fellowship (2022), and an NSF Career Award (2021).

Raghu Meka is a Professor of Computer Science at UCLA. Prof. Meka did his PhD at UT Austin and a postdoctoral fellowship at the Institute for Advanced Study, Princeton, and DIMACS, Rutgers University. Prof. Meka works at the intersection of probability theory, learning theory, combinatorics, and theoretical computer science. He is a recipient of IEEE's W. Wallace MacDowelll Award for 2025. He has also received a best paper award at the IEEE Symposium on Foundations of Computer Science (FOCS) 2023, and the Conference on Learning Theory (COLT) 2024.