7 papers
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…
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.