4 papers · 1 filter
ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems
Zeyu Zheng, Yiyang Liu, Yuyang Zhao +20
As AI systems begin to resolve open research problems, reliable verification becomes increasingly important. Formal mathematics provides a trusted framework for mathematical reason…
What is mathematics now, and what should it be?
Jeremy Avigad
Advances in neural theorem provers have been impressive, but the successes obscure a broader vision of what AI can do for mathematics and how mathematicians can engage with AI. Thi…
The Problem Is the Problem: Towards Scalable Mathematical Discovery
Zeyu Zheng, Shengtong Zhang, Jeremy Avigad +2
AI systems are increasingly capable of contributing to mathematical research. In research practice, frontier-model reasoning is a limited resource, and expert mathematical review i…
ImProver: Agent-Based Automated Proof Optimization
Riyaz Ahuja, Jeremy Avigad, Prasad Tetali +1
Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean. However, we often want to optimize a formal proof…