Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A beginning for mathematics

daniellitt.com

Post reply on HN
Print view View original

121–130 of 135 posts

Re: A beginning for mathematics

#121

Post by sigmoid10 »

MarceliusK wrote: post #117
wrs wrote: 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 by Jaxan »

Jblx2 wrote: post #37
Jaxan wrote: 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

Post by remus »

ComplexSystems wrote: post #58

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

Post by bell-cot »

GMoromisato wrote: post #110

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.

Re: A beginning for mathematics

#128

Post by bonoboTP »

jltsiren wrote: post #51
wrs wrote: 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. “…

An oral defense is ultimately a meeting, with the same weaknesses as other types of meetings. In particular, if new information comes up in a meeting, you cannot reasonably expect to get useful responses from the other participants. First impressions maybe, and plausible-sounding bullshit from those prone to generating that. If you want anything more, you need to provide the information in advance or schedule another…

And even then, the other examiner will only fail the candidate under egregiously extreme conditions. Rather, if the supervisor wants to pass someone who is unfit but not egregiously, this will just erode the supervisor's reputation among peers. Because there is a grapevine of course. So it can't be regular. But academics also really care about face and embarrassment, so they won't make a scene, u less there is preexisting drama around the supervisor. The only fails during the oral I've heard of happened when the candidate insisted to defend against their advisor's wish.

Re: A beginning for mathematics

#129

Post by bonoboTP »

remus wrote: post #123
ComplexSystems wrote: post #58

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

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

You're replying to a comment about "clean proofs" and explaining to humans. You talk about true/false anyway. Re-read please.

Re: A beginning for mathematics

#130

Post by bonoboTP »

curt15 wrote: post #89
cman1444 wrote: post #84

Earlier quoted context omitted.

I keep seeing people repeat that the goal of math is "understanding". I do think that is one goal of math but I don't think it's the only one. I think an additional goal is simply "truth", which can be found without understanding as we've seen with these human-incomprehensible proofs. Yet another is practical applications. While there's less of these in pure mathematics than in most domains, they do still exist.

The primary goal of all basic sciences is human understanding. "Truth" is no more a goal for mathematicians than the physical laws are a goal to physicists; they simply exist in nature. The goal is rather to develop useful language and conceptual frameworks for reasoning and communicating. That understanding underpins all practical applications.

Sciences don't have goals, people have goals and they differ. Some are fans of pure math as a kind of religious or almost erotic activity in elegance and beauty, others are application minded. Some are in it for the community and outreach and conferences, some are in it to just sit in an office alone and be left alone to do it in a zen like flow state all day and night. Some treat it as a 9-5 to pay the bills with a skill they happen to be fit for but aren't especially passionate about.
Post reply on HN