Hacker News Reader

Comment by gus_massa | Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com