Bridging Complexity and Automation to Advance Automatic Theorem Proving
The Project
This project automated theorem proving through three innovative research directions that address key conceptual questions about proof difficulty, tractability and performance scaling. In particular, this project will investigate and seek to formally define i) how difficult proving tasks can be from a computational complexity perspective; ii) how much data (real and/or synthetic) would be necessary to solve given proving tasks; and iii) how proof complexity evolves as a function of available computational resources.
The Team
Toniann Pitassi is the Jeffrey L. and Brenda Bleustein Professor of Engineering at Columbia University, in the department of Computer Science. Prior to joining Columbia in 2020, Pitassi was the Bell Canada Research Chair of Computer Science at the University of Toronto. Her primary research focuses on proof complexity, complexity theory, and foundational topics in machine learning, including privacy, fairness and adaptive data analysis. Pitassi is a member of the National Academy of Sciences, and a fellow of the ACM.
Richard Zemel is the Trianthe Dakolias Professor of Engineering and Applied Science in the Computer Science Department at Columbia University. He is the Director of the NSF AI Institute for Artificial and Natural Intelligence (ARNI), and was the Co-Founder and inaugural Research Director of the Vector Institute for Artificial Intelligence. He is a Canadian Institute for Advanced Research AI Chair and is on the Advisory Board of the Neural Information Processing Society. His research contributions include foundational work on systems that learn useful representations of data with little or no supervision; graph-based machine learning; and algorithms for fair and robust machine learning
Tianlong Chen is an assistant professor in the Department of Computer Science at the University of North Carolina at Chapel Hill. He received his Ph.D. degree from ECE at UT Austin in 2023 and had a postdoc at MIT and Harvard in 2024. His research focuses on efficient and reliable machine learning, large language model agents, multi-modal learning, and AI for Science.
Yanjun Han is an assistant professor of mathematics and data science in the Courant Institute of Mathematical Sciences and Center for Data Science at New York University. He received his Ph.D. in Electrical Engineering from Stanford University in 2021, and spent years at the Simons Institute for the Theory of Computing, UC Berkeley and the Statistics and Data Science Center at MIT. He is broadly interested in the mathematics of data science, including statistics, learning theory, bandits, and information theory.
Zhun Deng is an assistant professor in the Department of Computer Science at the University of North Carolina at Chapel Hill. He received his Ph.D. degree from CS at Harvard University in 2022 and was a postdoc at Columbia University from 2022- 2024. His research interests lie at the intersection of machine learning, theoretical computer science, and statistics. Recently, he is interested in AI for maths, human-AI collaboration, and agentic AI.