JUANA SUMMERS, HOST:
Mathematicians are struggling to figure out what to do with a flood of new results from artificial intelligence. As NPR's Geoff Brumfiel reports, a release by the company OpenAI is shaping up to be just a massive homework assignment.
GEOFF BRUMFIEL, BYLINE: Earlier this month, OpenAI threw up a repository filled with more than 370 results for longstanding problems in mathematics. Among them was one mathematician Dana Moshkovitz at UT Austin had been working on for years.
DANA MOSHKOVITZ: It's the Unique Games Conjecture. It's a terrible name because it has nothing to do with games.
BRUMFIEL: The Unique Games Conjecture is very abstract. It's a hard problem about approximating solutions to other hard math problems. It's considered among the most challenging in her area of study. And all you really need to know is that the AI solution, that proof it wrote...
MOSHKOVITZ: It looks right.
BRUMFIEL: Mathematicians around the world are in a state of shock. Over the past six months, AI has started doing what none of them thought was possible - proposing solutions for some of the toughest problems in the field. Things like the Unique Games Conjecture, which has been around for decades, are being solved in hours. But the solutions still need to be checked, and that's turning into a big headache because the AI-generated papers are a tough read.
MOSHKOVITZ: The write-up is terrible. The write-up is not made for human consumption.
BRUMFIEL: And it's not always right. Daniel Litt at the University of Toronto was initially really excited about a paper posted in his own field of algebraic geometry until he and others realized there was a problem.
DANIEL LITT: The error is quite subtle. It's like a sine error (ph), basically.
BRUMFIEL: But it means the whole paper is wrong. Litt is very excited about the future of AI mathematics, but he feels conflicted that the field is suddenly being tasked with checking what he describes as raw mathematical data.
LITT: You know, I'm certainly interested in some of the claims. I'm not super interested in, you know, cleaning up after a trillion dollar company's, well, whatever it is.
BRUMFIEL: To help with this assignment, mathematicians have turned to some non-AI computers. In recent years, a program called Lean has been used to check mathematical proofs. It works like this. A written proof is converted into Lean computer code. That code is then read by Lean to check if it's right. But there's a problem. Take a proof released last month by OpenAI. It may have solved one of the biggest questions in mathematics, a so-called Millennium Prize Problem. That proof was verified using Lean, but researchers have now found that the AI made unexpected changes to its work when it translated the proof into Lean. Anders Hansen is a professor of mathematics at the University of Cambridge. He showed me an equation where a four was switched to a five.
ANDERS HANSEN: Four or five. Who cares? Well, here's the problem. This statement here, which is what is in the natural language proof, is stronger than what Lean proofs.
BRUMFIEL: This mismatch doesn't mean the larger solution is necessarily wrong, but Hansen says all these proofs need human graders.
HANSEN: I would suggest that we should check them seriously.
BRUMFIEL: Last week, Anthropic and OpenAI announced they were committing around $5 million each to an initiative that would in part help researchers evaluate AI-assisted results. That support could help mathematicians dig through literally tens of thousands of poorly written AI-generated pages. But it can't address a much larger question. What is the job of a mathematician now? Dana Moshkovitz says she's not afraid of AI.
MOSHKOVITZ: It opens up amazing possibilities for math.
BRUMFIEL: But she's also not sure what to do next. She devoted a lot of time over the years to trying to solve the Unique Games Conjecture, and she was planning on spending even more.
MOSHKOVITZ: I mean, this was a life plan for me, right? And now it's gone, and I need to reevaluate.
BRUMFIEL: AI is changing her job forever. She's just not sure how.
Geoff Brumfiel, NPR News. Transcript provided by NPR, Copyright NPR.
NPR transcripts are created on a rush deadline by an NPR contractor. This text may not be in its final form and may be updated or revised in the future. Accuracy and availability may vary. The authoritative record of NPR’s programming is the audio record.
