If youre going to spend 10 million dollars on 10000 agents trying to solve some important maths problem I think it's reasonable to ask for some grants to help digest whatever they came up with.
Or you could hire mathematicians and do it in-house, but I guarantee you grants to PhD students are cheaper than silicon value salaries.
Not for now, but it's AI is getting better. A big step is "refactoring" a very long proof into a few intermediate lemas and theorems that are more inteligible and useful for other proof. It may take a few years or decades in some cases.
Anyway, I expect AI to be better at "refactoring", but for now a centaur is better.
Actually, for what you are mentioning, it is getting worse. There was a sweet spot somewhere around the release of GPT-o3, and ever since, the LLMs have been getting more accurate at solving problems, but worse at explaining how, and to hone in on what is interesting. This isn't surprising, as RL strategies shifted from RLHF to RLVR, so priorities during learning changed. I don't expect AI labs to reverse course on this. We can expect AI proofs to become increasingly incomprehensible over time.
I still remember Garry Kasparov vs. Deep Blue. Now, Magnus vs Stockfish is not even funny. I've seen AlphaGo and AlphaStar, and how their communities reacted...
I remember when Mathematica only could tell the answers and you had to type the formula correctly. Now there are apps that solve the exercise from a photograph with all the intermediate steps. We reminded the T.A. to be more alert during the midterms becuse we already had problems. I'm very worry about the magical glasses now, but it's important to be not overreact and be polite with the students.
Back to refactoring unintelligible long math proof: Let's talk again in 2031.
Animats · · focus · HN ↗
unddoch · · focus · HN ↗
ChickeNES · · focus · HN ↗
eli_gottlieb · · focus · HN ↗
gus_massa · · focus · HN ↗
Anyway, I expect AI to be better at "refactoring", but for now a centaur is better.
hodgehog11 · · focus · HN ↗
gus_massa · · focus · HN ↗
I remember when Mathematica only could tell the answers and you had to type the formula correctly. Now there are apps that solve the exercise from a photograph with all the intermediate steps. We reminded the T.A. to be more alert during the midterms becuse we already had problems. I'm very worry about the magical glasses now, but it's important to be not overreact and be polite with the students.
Back to refactoring unintelligible long math proof: Let's talk again in 2031.