The future of mathematics will be unthinkably many agents working together in harmony to expand the known corpus of knowledge. We are going to make unimaginable progress in the coming years towards solving old problems and discovering new ideas before they are quickly digested and moved on from. The pace of discovery will soon be too fast for even the best human mathematicians to keep up with.
In order for us to make this dream a reality, it is key to enable agents to have the right tools. One particular tool is search. Mathematics is largely about breaking a problem into smaller pieces which are more directly related to existing statements in the literature. AI agents need to have access to the latest collective knowledge in order for them to work together properly.
Taking a step back, much of the mathematics of the future may be formal. Proof assistants like Lean can check that a formal proof term has a claimed type relative to a specified collection of definitions and axioms. This does not guarantee that an informal statement was translated faithfully, that the axioms are consistent, or that an agent will never guess incorrectly; projects must also reject placeholders such as sorry. Within those boundaries, Lean gives AI agents a precise environment in which invalid formal proof steps are rejected by a small trusted kernel.
Albeit, one clear issue arises: When AI agents want to advance the field of mathematics by reasoning over data not strictly contained in their pretraining data, where will they get this information from? LeanExplore solves this issue by providing a searchable index of select Lean packages. Agents can search for declarations both by name, code, and informal meaning. This multifaceted approach enables agents to quickly find any relevant mathematics to their thoughts—just like us—much faster than manually going through the GitHub repositories themselves. Furthermore, in the forthcoming update to LeanExplore, we are going to support nightly updates, allowing agents to use the most recent Lean code.
I am extremely excited to see how far we can push formal verification.