Live data from Hacker News

A beginning for mathematics

daniellitt.com

121–124 of 124 posts

Re: A beginning for mathematics

#121
post #32

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.

Unfortunately, from my experience, forcing people to talk about their research to an audience mostly just condemns introverts and people with social anxiety. Being able to formulate your thoughts clearly in writing and in speech are two radically different skills. I've seen world class scientists give the most horrible conference presentations to the point where everyone in the audience agreed they'd rather have just read the paper when it came out, because they had no clue what he said while the author is amazing at writing. If we want to switch academia and to purely oral skills, you'll probably need to replace a ton of people. And in the industry these fields are already dominated by fast talking bullshitters.

Re: A beginning for mathematics

#122
post #37
post #29

Earlier 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…

With human proofs, I have some trust in process behind it.

Re: A beginning for mathematics

#123

I 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…

> Similarly now we're getting AI doing math. The proofs compile but are a mess. So just make the models better at writing clean proofs and explaining what they're doing to humans. That's the end of it.

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

#124

My 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?

> If today it takes twenty years of math study to reach the frontier ...

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.

Post reply on HN