The author argues for evaluating Ph.D. candidates based more on the oral thesis defense than on the actual thesis. By essentially the same reasoning, I’ve been arguing for prioritizing in-person design/code reviews over code-only async PR comments. The important thing is to verify that the human has a coherent design in mind and can demonstrate that it got implemented, regardless of who or what was at the keyboard. “…
The tricky part is that live review is much more expensive than async review. But maybe that just means we were getting away with a cheap proxy because it happened to work reasonably well.
A beginning for mathematics
121–124 of 124 posts
Re: A beginning for mathematics
#122Earlier quoted context omitted.
The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.
That seems like a red herring. Have you independently verified the human generated proof of FLT? Surely someone else will try to verify Anthropic's formalization on different hardware. Plus, it seems likely that FLT formalizations will improve / get shorter over time, requiring less compute. And computers (and type-checkers) will continue to get faster over time as well. So maybe in 5 years you could own a computer f…
Re: A beginning for mathematics
#123I admit I just don't understand this attitude. People had the same complaints that the code produced by early coding models was messy, lazy, poorly commented, had terrible architecture and so forth. The central complaint was that it was just too difficult for humans to review. The answer is just to improve the models and move on. Similarly now we're getting AI doing math. The proofs compile but are a mess. So just ma…
The assumption here is that the true/false of the theorem is the important outcome. While it is certainly part of it, a big part of maths is the understanding you gain from a proof. Many of the best proofs elegantly explain some aspect of the maths which was previously unclear and expand our understanding of the world.
To use a programming related example, imagine that an LLM spits out a solution to the travelling salesman problem which works in O(n) time. On the one hand that's very convenient for whatever problem you happen to be trying to solve at the time...but there's also an answer to P=NP in there! The former means your delivery drivers app works a bit faster on their busy days, the latter fundamentally shifts how humanity thinks about certain problems.
Going back to the maths, there have been theorems that were proved (by people) where the proof is broadly seen as 'unsatisfactory' in that it doesn't really expand our understanding. I assume some of these LLM proofs are a bit like that: we now know that the thing is true, but we really want to know why it's true, and how that changes our understanding.
Re: A beginning for mathematics
#124My worry is that the frontier of math is too far away for most humans to reach. AI is only going to make that worse. If today it takes twenty years of math study to reach the frontier (in a narrow field), what's it going to be like when it takes forty years? Or four-hundred years? Will the fields just get narrower and narrower to accommodate finite human intelligence?
Are you counting from when a kid first learn 1 + 1 = 2? That seems a misleading metric. The rate at which kids are learning math in the first half to 2/3 of their schooling is very low. Or are you asserting that Ph.D.'s don't reach the frontier until age 40+?
Actually, the frontier of math is too far away for most humans to reach because >99% of humans don't have the drive and talent to study and learn enough advanced math. Similar barriers exclude >99% of people from Olympic-level athletics, or being famed violinists, or being important architects, or being US Senators, or being successful ancient historians, or many other things.