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

The cultural divide between mathematics and AI

sugaku.net

Post reply on HN
Print view View original

171–180 of 187 posts

Re: The cultural divide between mathematics and AI

#171

Post by xg15 »

oersted wrote: post #42
xg15 wrote: post #22

> One question generated particular concern: what would happen if an AI system produced a proof of a major conjecture like the Riemann Hypothesis, but the proof was too complex for humans to understand? Would such a result be satisfying? Would it advance mathematical understanding? The consensus seemed to be that while such a proof might technically resolve the conjecture, it would fail to deliver the deeper understa…

Serious theorem-proving AIs always write the proof in a formal syntax where it is possible to check that the proof is correct without issue. The most popular such formal language is Lean, but there are many others. It's just like having a coding AI, it may write some function and you check if it compiles. If the AI writes a program/proof in Lean, it will only compile if the proof is correct. Checking the correctness…

Ah, thanks for the clarification. Then the whole thing makes a lot more sense - though I'd say the outlook also becomes more optimistic.

I thought the rhetoric sounded somewhat like the AGI/accelerationist folks who postulate some sort of eventual "godlike" AI whose thought processes are somehow fundamentally inaccessible to humans. So if you had a proof that was only understandable to this sort if AIs, then mathematics as a discipline of understanding would be over for good.

But this sounds like it would at least theoretically let you tackle the proof? Like, it's imaginable that some AI generates a proof that is several TB (or EB) in size but still validates - which would of course be impossible to understand for human readers in the way you can understand a paper. But then "understanding" that proof would probably become a field of research of its own, sort of like the "BERTology" papers that try to understand the semantics of specific hidden states in BERT (or similar approaches for GPTs).

So I'd see an incomprehensible AI-generated proof not as the end of research in some conjecture, but more as a sort of guidance: Unlike before, you now know that the treasure chest exist and you even have its coordinates, you just don't have the route to that location. The task then becomes about figuring out that route.

Re: The cultural divide between mathematics and AI

#172

Post by xanderlewis »

bwfan123 wrote: post #155

I had an aha moment recently. An excited AI researcher claimed, wow: claude could solve this IMO problem. Then, a mathematician pointed out a flaw which the AI researcher overlooked. The AI researcher then prompted the AI with the error and then the AI produced another proof he thought worked, but again was flawed. The AI played on the researcher's naivete. Long story short, current AI is doing cargo-cult math - ie,…

Everything you’ve said is obvious, and yet really needs saying and isn’t said enough.

Re: The cultural divide between mathematics and AI

#173

Post by zmgsabst »

nicf wrote: post #119
zmgsabst wrote: post #110

Earlier quoted context omitted.

CNCs and other technology haven’t destroyed woodworking. There’s whole communities on YouTube — with a spectrum from casual to hobbyist to artisanal to industrial. Why would mathematics be different than woodworking? Do you believe there’s a limited demand for mathematics? — my experience is quite the opposite, that we’re limited by the production capacity.

This is actually a metaphor I've used myself. I do think the woodworking community is both smaller and less professionalized than it would be in a world where industrial furniture production didn't exist. (This is a bizarre counterfactual, because it's basically impossible for me to imagine a world where industrial furniture production doesn't exist but YouTube does, but like pretend with me here for a moment.) I don…

That’s no different than high-end artisanal woodworking, which I would argue is comparable to self-directed, cutting-edge research:

- apprenticing

- journeyman phase

- only finally achieving mastery

CNC never replaced those people, rather, it scaled the whole field — by creating much higher demand for furniture. People who never made that full journey instead work at factories where their output is scaled. What was displaced was mediocre talent in average homes, eg, building your own table from a magazine design.

You still haven’t answered why you think mathematics will follow a different trajectory — and the only substantial displacement will, eg, be business analysts no longer checking convexity of models and outsourcing that to AI-scaled math experts at the company.

Re: The cultural divide between mathematics and AI

#174

Post by zmgsabst »

dinkumthinkum wrote: post #116
zmgsabst wrote: post #110

Earlier quoted context omitted.

CNCs and other technology haven’t destroyed woodworking. There’s whole communities on YouTube — with a spectrum from casual to hobbyist to artisanal to industrial. Why would mathematics be different than woodworking? Do you believe there’s a limited demand for mathematics? — my experience is quite the opposite, that we’re limited by the production capacity.

HN has this very unique and strange type of reasoning. You’re actually asking why would mathematics be any different than woodworking because CNC machines? It’s like aby issue can be reduced to the most mundane observations and simplicity because we have to justify all technology. Professional mathematics requires years of intense and usually, i.e. almost always, in graduate schools and the entire machinery of that.…

No Im not — I’m comparing two fields that range from hobby to professional, both of which I’ve worked in professionally. But for which automation occurred at different times.

> You’re comparing something many people do as a hobby to the life’s work and f others.

You’re denigrating the talents and educational efforts of artisanal woodworkers to make a shallow dismissal of my point.

Re: The cultural divide between mathematics and AI

#175

Post by zmgsabst »

jebarker wrote: post #153
zmgsabst wrote: post #108

Earlier quoted context omitted.

This seems obviously untrue: why would they be replicating it if they didn’t want it? I see both cases as people who aren’t well served by the artisanal version attempting to acquire a better-than-commoditized version because they want more of that thing to exist. We regularly have both things in furniture and don’t have any great moral crisis that chairs are produced mechanistically by machines. To me, both things s…

> why would they be replicating it if they didn’t want it? Who is "they"? Most AI for math work is being done by AI researchers that are not themselves academic mathematicians (obviously there exceptions). Similarly, most AI for music and AI for visual art is being done by AI researchers that themselves are not professional musicians or artists (again, there are exceptions). This model can work fine if the AI researc…

> This model can work fine if the AI researchers collaborate with mathematicians or artists to understand that the use of AI is actually useful in the workflow of those fields, but often that doesn't happen and there is a savior-like arrogance where AI researchers think they'll just automate those fields.

In my experience, the vast majority is people who are hobbyists or amateurs in those fields, who are looking to innovate in approaches — eg, the overwhelming majority of AI music is hobbyists using models to experiment. Similarly, the overwhelming majority of people using AI graphics tools are making memes or pictures to share with friends.

Those people are poorly served by the artisanal approach and are looking to create more art — they’re not engaging in “savior-like arrogance” but trying to satisfy unmet desire for new music and art. You’re merely being snooty.

> But in the case of art, and I (and Hardy) would argue academic math, there's a human aspect that can't be removed.

This is the pretentiousness I called out (and you completely failed to address):

> That’s the need that, eg, automated theorem proving truly solves — and mathematicians are being ignored (much like artist) by people they turn up their noses at.

Nobody is stopping you from your artisanal proofs — have at it. You’re refusing to do the ugly work people actually want, so they’re solving their problems with a tool that doesn’t involve you.

Re: The cultural divide between mathematics and AI

#176

Post by lacker »

roenxi wrote: post #120
rssoconnor wrote: post #99

Earlier quoted context omitted.

I do think the why that the Four Colour Theorem is true is captured my statement. The reason why it is true is because there exists some finite unavoidable and reducible set of configurations. I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I suspect that if the size of this finite set were 2, instead of 633, and you could draw these unavoidable configuration o…

> I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I think that is exactly correct, except for the "no good reason" part. There aren't many (any?) practical situations where the 4-colour theory's provability matters. So the major reason for studying it is coming up with a pattern that can be used in future work. Having a pattern with a small set (single digit nu…

To me, the four-color theorem is a very interesting proof of concept, perhaps the most interesting mathematical proof of the past 50 years. Perhaps the "pattern that can be used in future work" is the idea of having computers enumerate a large number of cases, which they then solve in individually straightforward ways.

But, I can understand if pure mathematicians don't feel this way. This might be only really an intriguing and beautiful concept to someone who is interested in scaling up algorithms and AI.

Re: The cultural divide between mathematics and AI

#177

Post by lacker »

seanhunter wrote: post #158
rssoconnor wrote: post #99

Earlier quoted context omitted.

I do think the why that the Four Colour Theorem is true is captured my statement. The reason why it is true is because there exists some finite unavoidable and reducible set of configurations. I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I suspect that if the size of this finite set were 2, instead of 633, and you could draw these unavoidable configuration o…

> The reason why it is true is because there exists some finite unavoidable and reducible set of configurations. OK but respectfully that's just restating the problem in an alternative form. We don't get any insight from it. Why does there exist this limit? What is it about this problem that makes this particular structure happen?

Perhaps the key insight is that there is no concise explanation that underlies this particular structure. Many mathematical statements are true for no concise reason. If you want to discover if these things are true or not, perhaps you need a computer-assisted search, and that's the intellectual lesson to be drawn here.

Re: The cultural divide between mathematics and AI

#178

Post by oersted »

xg15 wrote: post #171
oersted wrote: post #42

Earlier quoted context omitted.

Serious theorem-proving AIs always write the proof in a formal syntax where it is possible to check that the proof is correct without issue. The most popular such formal language is Lean, but there are many others. It's just like having a coding AI, it may write some function and you check if it compiles. If the AI writes a program/proof in Lean, it will only compile if the proof is correct. Checking the correctness…

Ah, thanks for the clarification. Then the whole thing makes a lot more sense - though I'd say the outlook also becomes more optimistic. I thought the rhetoric sounded somewhat like the AGI/accelerationist folks who postulate some sort of eventual "godlike" AI whose thought processes are somehow fundamentally inaccessible to humans. So if you had a proof that was only understandable to this sort if AIs, then mathemat…

In terms of having the proofs be understandable to humans, I'd say that's still a challenge. Not a fundamental challenge, but a real practical challenge still.

Lean makes the proofs verifiable, and sure to a degree understandable, but normal Lean proofs written by humans are already a challenge to understand without additional documentation, and, as with all code-generation, AI generated proofs are probably even harder to understand. There are many paths to arrive at a proof, the AI may take very messy routes that don't align with how humans create abstractions and assign meaning to break the process down into understandable steps.

In a sense all AI is understandable, nothing is hidden, you can see all the numbers inside a Transformer. Just being able to see the code might not necessarily help mathematicians too much in extracting deeper meaning and lessons from AI-generated proofs, at least not without significant additional work.

Re: The cultural divide between mathematics and AI

#179

Post by oersted »

xg15 wrote: post #171
oersted wrote: post #42

Earlier quoted context omitted.

Serious theorem-proving AIs always write the proof in a formal syntax where it is possible to check that the proof is correct without issue. The most popular such formal language is Lean, but there are many others. It's just like having a coding AI, it may write some function and you check if it compiles. If the AI writes a program/proof in Lean, it will only compile if the proof is correct. Checking the correctness…

Ah, thanks for the clarification. Then the whole thing makes a lot more sense - though I'd say the outlook also becomes more optimistic. I thought the rhetoric sounded somewhat like the AGI/accelerationist folks who postulate some sort of eventual "godlike" AI whose thought processes are somehow fundamentally inaccessible to humans. So if you had a proof that was only understandable to this sort if AIs, then mathemat…

There's an argument to be made that incomprehensible proofs are still very useful.

I understand that mathematicians are all about understanding why a theorem is true, not just checking that it is, and then using that understanding to push forward other research. Same as most scientists care more about understanding how the world works rather than developing methods to control and manipulate it.

But proven theorems are mathematical tools that can be used to make progress, regardless of your understanding of how they work. I think there is a path forward for maths as an engineering discipline, possibly with much faster progress, just as computer science expanded into software engineering. AI is just the next step of many, software libraries, interfaces and abstractions are also black-boxes in a sense that do stuff for you without knowing how.

A good engineer learns to build on the shoulders of giants, mastering the understanding of what tools do and how they behave, without necessarily needing to know how they are built from scratch. It might be less satisfying to the curious, but you can get a lot more done.

Re: The cultural divide between mathematics and AI

#180

Post by pathsjs »

trostaft wrote: post #151

> Unlike many scientific fields, mathematics has no concept of "first author" or "senior author"; contributors are simply listed alphabetically. I don't think this is (generally) true? Speaking as a math postdoc right now, at least in my field of computational mathematics there's definitely a notion of first author. Though, a note of individual contributions at the bottom of the paper is becoming more common.

Computational mathematics may have adopted conventions from computer science, but I assure you that the alphabetical order convention is definitely the standard in most pure mathematics (with some exceptions, such as the Ascoli-Arzelà theorem)
Post reply on HN