4 citations · 7 across the 8 of their papers we have counts for
9 papers
Advancing Mathematics Research with AI-Driven Formal Proof Search
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to gener…
An Improved Last-Iterate Convergence Rate for Anchored Gradient Descent Ascent
Anja Surina, Arun Suggala, George Tsoukalas +5
We analyze the last-iterate convergence of the Anchored Gradient Descent Ascent algorithm for smooth convex-concave min-max problems. While previous work established a last-iterate…
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Austin Letson, Leopoldo Sarra, Auguste Poiroux +9
We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed…
Learning Interestingness in Automated Mathematical Theory Formation
George Tsoukalas, Rahul Saha, Amitayush Thakur +2
We take two key steps in automating the open-ended discovery of new mathematical theories, a grand challenge in artificial intelligence. First, we introduce , a rein…
CLEVER: A Curated Benchmark for Formally Verified Code Generation
Amitayush Thakur, Jasper Lee, George Tsoukalas +6
We introduce , a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean. Each problem consists of (1) the task of ge…
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
Amitayush Thakur, George Tsoukalas, Greg Durrett +1
Neural approaches to theorem proving require robust infrastructure for interfacing with interactive theorem provers (ITPs), extracting structured proof data, and executing proof se…
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
George Tsoukalas, Jasper Lee, John Jennings +5
We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692…
An In-Context Learning Agent for Formal Theorem-Proving
Amitayush Thakur, George Tsoukalas, Yeming Wen +2
We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-art models for the problem are finetuned on environment-s…
-NIM trees: Characterization and Enumeration
Charles R. Johnson, George Tsoukalas, Greyson C. Wesley +1
Among those real symmetric matrices whose graph is a given tree , the maximum multiplicity that can be attained by an eigenvalue is known to be the path cover number of $…