Mathematicians explore ideas by proposing conjectures and proving them with theorems. They have carefully constructed these proofs line by line over centuries. And most mathematics researchers still work that way. However, artificial intelligence is fundamentally changing this process. AI assistants called “co-pilots” are starting to help mathematicians create proofs. There is a real possibility that this could one day allow humans to answer some questions that are currently beyond our brains.
One promising type of AI co-pilot is being developed at the California Institute of Technology. It automatically suggests the next step in a proof, helps you complete intermediate mathematical goals, and helps build logical connective tissue between larger steps. “If you’re developing a proof, this new co-pilot gives you multiple suggestions for how to proceed,” said Animashree Anandkumar, professor of computing and mathematical sciences at Caltech. I am. Anandkumar and his team presented AI co-pilots in a recent preprint paper that has not yet been peer-reviewed. Importantly, these suggestions “all would be correct,” she says.
The co-pilot is a large-scale language model (LLM), the same type of machine learning system behind OpenAI’s ChatGPT and Google’s Gemini. Although the training is different, it is also similar to the technology behind Google’s AlphaProof and AlphaGeometry 2. Both produced complex mathematical proofs for the world’s best high school students that reached silver medal standards at this year’s International Mathematics Olympiad (IMO). Also, while LLM can generate what could technically be called “bullshit,” the co-pilot’s false suggestions are checked and rejected. In the case of the Caltech co-pilot, that’s thanks to AI-powered software called “Lean,” which uses rigorous mathematical logic to filter out valid statements.
About supporting science journalism
If you enjoyed this article, please consider supporting our award-winning journalism. Currently subscribing. By subscribing, you help ensure future generations of influential stories about the discoveries and ideas that shape the world today.
Proof by code
Over the past few years, Lean has become increasingly popular and has a small but growing user base. This open source software allows mathematicians to input mathematics through coding. This process is known as formalization. What are the benefits? You can’t go wrong with that. In Lean and other proof assistant applications, the software automatically checks the accuracy of mathematical statements. This is a world apart from traditional so-called informal mathematics, where reviewers and colleagues painstakingly audit pages of such writing. This process is prone to human error and mistakes can go unnoticed.
If you’re writing a proof with the help of a Caltech copilot, you can click a button to request a new line in the Lean programming language that represents the mathematics you’re working on. Several options, which Anandkumar refers to as “tactical suggestions,” will appear on the right side of the screen. All you have to do now is choose the option that seems most appropriate. If the proof is heading in a direction with obvious or well-known intermediate conclusions, the co-pilot can also suggest ways to complete that trajectory.
Martin Heiler, a professor of pure mathematics at the Swiss Federal Institute of Technology in Lausanne and Imperial College London, said Lean “doesn’t have reliability issues” because the software checks the work. Still, many scholars have not yet adopted it. “It’s difficult to use because you have to enter all the math as code,” Hairer says. Coding with Lean requires entering details that are omitted when writing a paper, so stating a self-evident truth or something self-evident can require multiple pages of code, he said. Point out.
But Hairer, who is not involved in the Caltech project, believes an AI co-pilot will eventually take over all that heavy lifting. “Once you present a statement that is obvious to most mathematicians, LLM should be able to generate the code for it,” he says, adding that speeding up this process “could tempt a new generation of mathematicians to Lean.” added.
Anandkumar also predicts that more researchers will adopt formal AI-assisted mathematics. “When you talk to young mathematicians and early-career undergraduates today, you find that they are familiar with these AI systems,” she says. “They will do whatever it takes to make their jobs faster and easier to be competitive.”
mathematical transformation
These platforms need to become even more powerful before the international mathematics community can adopt AI tools in a meaningful way. Google’s AlphaProof and AlphaGeometry 2, which earned silver medal standards at this year’s IMO, showed impressive results. However, they are still not at the level that research mathematicians need to support complex proofs. In that respect, humans are still better mathematicians.
But “systems that approach that level will soon emerge,” says David Silver, vice president of reinforcement learning at Google DeepMind. “I think this essentially elevates human mathematicians to a place where they can operate at a higher level and think through ideas.” Mathematics is starting to change, just as it was when electronic computers were invented. he says. “In the days before calculators, there was a wide range of mathematics that was very tedious and required a lot of effort,” he says. “I think we are now in the proof stage. In the future, very complex proofs will be automatically solved by AI.”
Collaboration using AI
The adoption of AI co-pilots will also revolutionize the way mathematicians collaborate with each other. Usually they act alone or in small groups. A trusted colleague evaluates each proof. But formal AI assistants could enable large groups of human collaborators to tackle the largest problems by breaking them down into sub-problems. Each part is batched to be solved by different teams specializing in AI and human partnership. “Mathematics has been seen as a solitary endeavor, especially in popular media, but now AI looks like it will be an enabler for collaboration between mathematicians,” Anandkumar says.
Mathematicians are generally optimistic that AI co-pilots will soon give human experts a boost, allowing them to invest their time on more complex and difficult problems. For example, in the coming years, AI-human partnerships may take on the notoriously difficult Millennium Prize problems. Perhaps even something as difficult as P vs. NP is a long-standing question in theoretical computer science, asking whether all problems can be solved. It can be quickly verified and resolved quickly.
“That’s where we end up quickly,” Silver says, thinking about the concept of solving such questions. “Complex problems like ‘P vs. NP’ or equally difficult problems are way beyond our level today in terms of even knowing how to start,” he says. . “But I can imagine that maybe within three years, we might be moving in that direction.”
