AI for math is a hot topic right now, as it has shown to be powerful but also controversial in many ways. This is a summary of my thoughts regarding the most prominent discussion points today:
- I have been hearing the argument that math is not about the true/false verdict of a particular statement but rather about the math invented along the way in investigating that problem. While the journey to a result undoubtedly progresses math further, I would argue the result itself is important too. Math is the foundation of science, science is the foundation of engineering, engineering is the foundation of technology. Any new knowledge, even just a true/false verdict, is something that we can build on top of in this chain and that gives us more confidence in prediction. We can accept AI-generated results by themselves (when they are formally verified), while in parallel working to understand the proofs ourselves and go further using that understanding.
- Relatedly, the math community culture can over-emphasize novelty and over-use labels like “trivial.” Then, “trivial” knowledge ends up not being mentioned though it is “well-known,” and people end up re-treading the same paths, which is wasteful. This is especially the case for knowledge that is trivial from more powerful vantage points (e.g. category theory) but is non-obvious in other contexts. We should be as inclusive as possible in the “corpus of humanity’s knowledge,” and that should include AI-generated results in and of themselves; we should not block something because it doesn’t yet satisfy human-understanding requirements.
- We should not define mathematicians’ or in general people’s purpose by whether work exists for them to do. In the chain of insight that starts from math and leads to technological progress, whatever part AI can (reliably) do faster than humans, we should let it. For example, in the case of curing disease, requiring humans to review parts of the chain that can be AI-generated and formally verified would slow things down and be irresponsible. I’m not sure how people can be taken care of economically if novel work doesn’t exist, but the general solution has to support no-novel-work and not involve artificially creating work.
- Anyway, right now, there is still ample work remaining in exposition and communication, assuming AI can discover novel math more effectively than any human. Many other authors have written about this; for example, see Grant Sanderson’s post.
- Regardless of what AI solves, humans should allot themselves space to try out problems themselves — this is important for cognitive “exercise,” the same way we go to the gym despite forklifts existing. This also opens up new avenues for insights even for problems already solved by AI; results often have multiple proofs for this reason.
- There is a lot of value AI can provide in math beyond novel research. For example, as I argued in this post, published math papers are written informally from a computer verification perspective, so they must be verified by humans, who can make mistakes and have limited bandwidth, leading to bias against “non-established” researchers. AI can “convert” such informal papers to Lean or other formally verified code by “filling in the informal gaps” (think “Similarly …”), essentially serving as automated peer review for math. Or as I argued in this post, AI can enable a “reverse search” where a researcher asks “is there a name already for [this definition]?” or “does [this theorem] have a name already?”, speeding up learning and communication.
- As the Navier-Stokes priority dispute shows, we need models that can provably track sources comprehensively and cite all influences without missing anything, to the level of academic publishing standards expected of any human. This is a promising area of development now.
- Philosophically, I consider anything AI generates to be part of humanity’s knowledge too. Humanity created AI as another of humanity’s technological tools, the same way that we created the microscope and used that to further biology but we still consider anything discovered using the microscope to be part of humanity’s knowledge. AI, and anything discovered using it, is still part of humanity’s enterprise, as much as with a microscope or telescope.
I am actually working on a new AI for math project that implements some of these ideas, starting with automated peer review with space for cognitive exercise — it doesn’t e.g. do auto-complete or otherwise auto-invoke AI, it only invokes AI upon request, so the user can do their cognitive exercise as much as they want and only get AI’s input at the very end. It aims to be complementary, not a replacement, to the incredible work that is already happening in this space. I will publish more details soon; I’d love to work with other people to see how we can contribute to this exciting area. We are in a transformational moment for math that can really unlock value for the better, let’s embrace it wholeheartedly and take on the important work ahead!
—
I’ll now elaborate on some of my points further with examples.
(Disclaimer: I haven’t yet studied some of these examples too deeply, so some of the details could be wrong, but I still stand by my main points.)
For the point that results matter by themselves too, consider the recently solved Navier-Stokes equations problem. The problem asks whether our current widely used physics theory for the behavior of fluids (Newtonian mechanics) actually leads to reasonable results in all relevant scenarios. Because we now have a negative answer to that, verified in Lean, even if we don’t know how the AI arrived at that answer or how we could come up with that answer ourselves (the process/journey), we immediately have more information than earlier to judge such a widely used theory and refine which theories we should use for which scenarios. This helps us refine our understanding of nature and how to predict it, which unlocks better opportunities for what we can build using this improved knowledge, as well as gives us greater confidence in our inventions given the increased accuracy of predictions. For Navier-Stokes, either the scenarios of failure that the AI identified should be now identified as unrealistic (and the negative answer makes us more aware of this as we revisit those cases, refining our criteria for judging theories), or we need to amend the fluid dynamics laws in those scenarios.
Furthermore, such extreme-case physics/science actually ends up being very important even for “everyday” technologies, often popping up in ways we may not initially expect. For example, cryogenic physics, which is physics at the lowest temperatures (far below “room temperature” or what humans would often encounter), was nevertheless fundamental for the invention of refrigerators, freezers, food preservation methods, and so on. As another example, quantum physics, which is physics at the smallest scales, may not be something we think we encounter in our daily lives, but some of our most important technologies today like computers were invented fundamentally using our knowledge of it.
Speaking of quantum mechanics, another Millennium Problem known as the Quantum Yang-Mills problem asks whether quantum physics may actually be logically contradictory (not well-defined) in certain relevant scenarios. A negative answer to this question, verified formally in Lean, even if we don’t understand how the AI arrived at it, would then give us insight into the limitations of predictive power of quantum physics, implying that it needs to be replaced in the failure scenarios that the AI was able to identify. On the other hand, a positive answer would give us greater confidence in quantum physics and enhance our understanding of it further.
Regarding applications of AI in math beyond novel research, we are seeing these progress as well now, e.g. Anthropic’s formalization of Fermat’s Last Theorem as well as Axiom’s formalizations of many human mathematicians’ papers. I have also seen “reverse search” capabilities in existing models I have tried out, but I’m not sure that these are for-sure comprehensive given that last I checked, such a reverse search would hallucinate sometimes too. While models are progressing rapidly, I’m not sure that “the models are getting better so you can trust them” is enough for the fidelity expected for math; instead, some kind of math-optimized open model with corresponding proof of accuracy and comprehensiveness of reverse search would be desirable.