Mathematicians’ Newest Assistants Are Artificially Intelligent
Mathematicians explore ideas by proposing conjectures and proving them with theorems. For centuries, they built these proofs line by careful line, and most math researchers still work like that today. But artificial intelligence is poised to fundamentally change this process. AI assistants nicknamed “co-pilots” are beginning to help mathematicians develop proofs—with a real possibility this will one day let humans answer some problems that are currently beyond our mind’s reach.
One promising type of AI co-pilot is being developed at the California Institute of Technology. It can automatically propose next steps in a proof and help complete intermediate mathematical goals, helping build the logical connective tissue between larger steps. “If I’m developing a proof, this new co-pilot gives me multiple suggestions for going forward,”says Animashree Anandkumar, a computing and mathematical sciences professor at Caltech. Along with her team, Anandkumar presented the AI co-pilot in a recent preprint paper, which has not yet been peer-reviewed. Crucially, she says, those suggestions “will all be correct.”
The co-pilot is a large language model (LLM), the same kind of machine-learning system behind OpenAI’s ChatGPT and Google’s Gemini. While its training is different, it is also similar to the technology powering Google’s AlphaProof and AlphaGeometry 2—both of which generated complex mathematical proofs to a silver medal standard at this year’s International Mathematical Olympiad (IMO) for the world’s best high school students. And although LLMs can generate what is, in a technical sense, “bullshit,” a co-pilot’s erroneous suggestions are checked and rejected. In the case of the Caltech co-pilot, that’s thanks to the software in which the AI operates, called Lean, which uses rigorous mathematical logic to screen for valid statements.
