8 papers
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…
Mathematicians in the age of AI
Jeremy Avigad
Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technol…
LeanArchitect: Automating Blueprint Generation for Humans and AI
Thomas Zhu, Pietro Monticone, Jeremy Avigad +1
Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are ce…
Is Mathematics Obsolete?
Jeremy Avigad
This is an essay about the value of mathematical and symbolic reasoning in the age of AI.
Anatomy of a Formal Proof
Jeremy Avigad, Johan Commelin, Heather Macbeth +1
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a compu…
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…