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

After Math

terrytao.wordpress.com

Post reply on HN
Print view View original

121–130 of 171 posts

Re: After Math

#121

Post by bbor »

yazaddaruvala wrote: post #12

I think as a civilization we need to postulate a new term: “purpose death” Defined something like: temporary state of complete loss of personal purpose and the experience of existential dread from never achieving self-actualization in spite of the tremendous time commitment towards excellence in a now automated intelligence. I truly think because of the pace of innovation this will be a universal feeling for every hu…

That is the definition of an existential crisis, btw. I like the neologism too, tho

Re: After Math

#122

Post by anonymouz »

auggierose wrote: post #119
anonymouz wrote: post #113

Earlier quoted context omitted.

Maybe, but it's not worth discussing the content if you dont comprehend what the authors are actually saying.

Here is what they are saying: 1. AI really did solve a problem in mathematics. The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. Yes, it is sufficient. To say otherwise is just goalpost shifting because you don't like the answer. There are, in fact, two notions of proof: a logical notion and an intelligible notion. Wro…

There is a point in distinguished a formal proof from an intelligible one, notwithstanding the fact that one can, with effort, be extracted from another. That's a key point of the discussion that we mathematicians are having now, and fits into the bigger question as to what it means to gain mathematical understanding. In fact, Tao happens to have some older posts about this himself. The naive formalist reduction that you are making is not really bringing us forward in having a useful reflection about this, as the discussion is already beyond that.

Re: After Math

#123

Post by bbor »

Sad to see such smart people with such small visions for the future.

  In mathematics, it is more natural to treat AI as an assistant rather than as a competitor. As Jeremy Avigad (2026) puts it, “We should keep in mind that AI is nothing more than technology, designed to serve our purposes. It is misguided to think of mathematicians as competing with AI; when we drive a car, we aren’t competing to see who can go faster, and when we use a phone, we aren’t competing to see who can speak louder.”
Like… surely I don’t need to explain why artificial minds are a unique invention?

Re: After Math

#124

Post by casey2 »

yazaddaruvala wrote: post #12

I think as a civilization we need to postulate a new term: “purpose death” Defined something like: temporary state of complete loss of personal purpose and the experience of existential dread from never achieving self-actualization in spite of the tremendous time commitment towards excellence in a now automated intelligence. I truly think because of the pace of innovation this will be a universal feeling for every hu…

But this is mathematics, modern mathematics had it's purpose death decades if not centuries ago. People got into it over the last 60-100 years for autistic reasons, now that AI has got rid of those reasons you'd have to be even more autistic to entertain the idea. But plenty of people are, and more tech = more mental illness so it'll probably be a wash.

Re: After Math

#125

Post by auggierose »

anonymouz wrote: post #122
auggierose wrote: post #119

Earlier quoted context omitted.

Here is what they are saying: 1. AI really did solve a problem in mathematics. The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. Yes, it is sufficient. To say otherwise is just goalpost shifting because you don't like the answer. There are, in fact, two notions of proof: a logical notion and an intelligible notion. Wro…

There is a point in distinguished a formal proof from an intelligible one, notwithstanding the fact that one can, with effort, be extracted from another. That's a key point of the discussion that we mathematicians are having now, and fits into the bigger question as to what it means to gain mathematical understanding. In fact, Tao happens to have some older posts about this himself. The naive formalist reduction that…

> There is a point in distinguished a formal proof from an intelligible one,

Fine, do that if you want. What you cannot do is call a logical and formal proof of a problem not solving the problem in mathematics. That is absurd, and mathematicians that insist on this are absurd, too. Note that Tao didn't say this, but two guests.

I understand that you might want more than a formal proof generated by a machine, just like I want fries with my steak. But saying that the steak is not food, is just ridiculous.

You are not further along in the discussion, you are having the wrong discussion. What is at stake here is nothing less than the question: Is mathematics subjective or objective? This mathematician thinks it is objective.

Re: After Math

#126

Post by pcfwik »

QuesnayJr wrote: post #111
charcircuit wrote: post #31

>The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. What is missing is an intelligible proof that human mathematicians can understand and use to advance the aims of mathematics. This makes a bad assumption that humans need to be the one to advance the aims of mathematics. LLMs could be what advances the aims of mathemat…

This is exactly backwards. Mathematics predates the idea of formal proof by millenia. The purpose of proofs since Euclid is to explain to your fellow human why something is true. The idea that the purpose of math is formal proof alone is a new idea that (some) computer programmers want to impose on the field (for the understandable reason that it makes computers primary). Formal proof only emerged early in the 20th c…

I broadly agree with your sentiment and am saddened (outraged?) to see the financially motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing.

However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong:

> Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...]

You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.)

What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic.

Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.

Re: After Math

#127

Post by stabbles »

sigmoid10 wrote: post #68

This kind of argument is always dangerous, because it essentially resorts to moving goalposts. "Oh, AI can now do X? Sure it is amazing, but it can't do Y yet, so we're totally safe!" Just because humans can't process the proof or see the advancements, it doesn't mean that it will remain that way in the future or that it will not change the field. If you only define yourself by things AI can't do yet , you're about t…

Strongly reminiscent of God of the Gaps [1]

[1]: https://en.wikipedia.org/wiki/God_of_the_gaps

Re: After Math

#128

Post by busyant »

> Terence Tao (2026) lists many goals of mathematics beyond problem solving. These include developing new theories and techniques, understanding the world, sustaining a community, training the next generation of mathematicians, contributing to cumulative knowledge, and creating works of aesthetic value. Of course, these have been positively correlated with genuine solutions.

> If, instead, mathematicians treat AI as a technology for advancing its long-standing and centrally human purposes, the technology may come to contribute to an accelerated flourishing and enrichment of the discipline.

For the longest time, people who conducted research (not just math) ranked and measured their peers (albeit quasi-subjectively) by 1.) their ability to solve difficult problems, 2.) the cleverness of their solutions, and 3.) the clarity of their explanations.

With the advent of these models, we're understandably worried because #1 and maybe #2 may be gone (maybe even #3).

Are researchers going to shift the ranking/measuring of their peers over to ... "so-and-so is a world-class explainer of AI proofs"?

If you go around telling people, "no no no. You don't understand. The important part of our intellectual work is now going to be ", well, then it feels like you're handing me a participation trophy and telling me I came in 1st place.

I have no idea how the next 5 years will shake out, but I think that's why there's a lot of anxiety at the moment.

Re: After Math

#129

Post by kaffekaka »

sigmoid10 wrote: post #68

This kind of argument is always dangerous, because it essentially resorts to moving goalposts. "Oh, AI can now do X? Sure it is amazing, but it can't do Y yet, so we're totally safe!" Just because humans can't process the proof or see the advancements, it doesn't mean that it will remain that way in the future or that it will not change the field. If you only define yourself by things AI can't do yet , you're about t…

The authors are absolutely not saying "we are totally safe". They are not denying that AI will affect math deeply in the short and the long run.

Re: After Math

#130

Post by matherial »

doctor_phil wrote: post #22
matherial wrote: post #11

Earlier quoted context omitted.

It might feel that way, but I'll ask again: where's the payoff? Where's all the amazing software that everyone is now supposedly shipping 10x faster than before? If I look at the software I'm actually using day-to-day, or that my friends are using, all this stuff looks exactly the same as it did in 2021. Not a single product release from Google, Microsoft, or more scrappy companies in the past 6 months made me go "wo…

From personal experience in a small (total <10 people) company, we have definitely 10x our product in the last two years. What 4 devs did in 4 years have been dwarfed by what 2 devs were able to do in 1 year with AI. I'm not so familiar with the giant companies, but from afar it seems like they already have practically all the code-writing capacity they wanted anyway. Google could say "let's build a browser" or "let'…

Again, I've heard that countless times on HN. Every time you ask, everyone is 10xing it and building amazing things that will go to market very soon now. But it's been a while; where is it? Somehow, everyone is just sitting on all these revolutionary advances while selling the exact same stuff as they were selling before, with the same warts and the same annoyances. Gmail is the same, Chrome is the same, Photoshop is the same, Slack is the same, Excel is the same... the only thing that seems to have changed is how SWEs feel about their jobs.
Post reply on HN