2 citations · 2 across the 3 of their papers we have counts for
7 papers
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…
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…
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…
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…
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…