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, the mathematics of the future is formal. Coding languages like Lean allow us to check whether mathematical proofs are 100% correct through a process called formal verification. By converting the informal mathematics into runable Lean code, we can guarantee the correctness of the logic. In turn, Lean allows AI agents to have an infinite playground to think and test the validity of their thoughts and logic. Current AI struggles on checking that the individual steps in their multistep thought-processes are correct. Lean completely resolves this issue, preventing any sort of guessing or hallucinations.

  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 (cf. also the preprint). 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—thanks, in part, to the wonderful work of Auguste Poiroux and others on the LeanREPL and LeanInteract—LeanExplore is going to support live real time updates whenever a commit is made. This means that agents will be able to search both the most recent Lean repositories and prior versions.

  I am extremely excited to see where this technology takes us.