9 ms·
As a mathematician maybe I am a little more optimistic than this declaration. I am thinking of Mochizuki's abc conjecture: He worked in relative isolation, an
by tmhn2 21d ago
As a mathematician maybe I am a little more optimistic than this declaration.
I am thinking of Mochizuki's abc conjecture: He worked in relative isolation, and dumped a huge incomprehensible proof on the community (to oversimplify a bit). That's not totally unlike what might happen if AI generates a huge, incomprehensible proof of let's say RH.
Well, what is the result? In the Mochizuki case, it was a lot of skepticism, but it also generated conferences, papers, talks in the hallway, discussions with students, and so on--a flurry of exactly that kind of community process that the declaration says is the main driver of mathematics.
Ultimately we think a fatal flaw was found in Mochizuki's proof, so it didn't lead anywhere in particular. But in our hypothetical "AI lean-verified proof of RH" situation, it would presumably generate substantially more of that community activity we saw in the Mochizuki situation. And if it's correct, that community activity would be productive (expository talks, students given problems to flesh out or generalize, etc).
Maybe mathematics just becomes a little more like other fields--relying on labs with lots of money for compute, digging through a corpus of AI-generated proofs, etc.
- num42 21d ago>Maybe mathematics just becomes a little more like other fields--relying on labs with lots of money for compute, digging through a corpus of AI-generated proofs, etc. Dr. Tao said the same thing. Somehow, this letter came through. He wants to conduct Math competitions where participants who don’t have formal credentials can contribute to mathematical research through AI. Title: Terence Tao - SAIR Competitions and the Future of Experimental Mathematics https://www.youtube.com/watch?v=rB9YOi3lb7w https://www.youtube.com/watch?v=rB9YOi3lb7w and this: Daniel Litt - Working with LLMs to do high quality math https://www.youtube.com/watch?v=0wL8NlhxXcU https://www.youtube.com/watch?v=0wL8NlhxXcU
- cubefox 21d ago> Dr. Tao said the same thing. Apparently he has since changed his mind.
- ksoped 21d agoDid he say so somewhere? I don't think these ideas are contradictory. It's just an pro AI tooling but anti-slop stance.
- cubefox 21d agoWhere is the difference?
- SpicyLemonZest 21d agoHe sees value in mathematicians using AI to carefully study mathematics, develop an understanding of both old and new things, and help others understand the new things. He doesn't see value in scrolling through unsolved problems asking an AI to please solve them. In his view, this is a fundamental confusion about what mathematical research is for. Knocking down unsolved problems without developing the community's understanding of them is like prompting Claude to go through a Jira board, write code for all the open tickets, and then close them without merging or deploying the code.
- bluecheese452 21d agoIsn’t it more like it merges the code without a dev reviewing or understanding it?
- SpicyLemonZest 21d agoNo. Merged code can perform actions with effects on the world, even if a human being never saw it. Constructing a giant Lean formalization that nobody understands simply doesn't do anything.
- dbmikus 21d agoPretty close, but IMO not quite. A math proof in and of itself is useless unless either: (A) it furthers human knowledge (B) it gets used in applied sciences, engineering, etc. If you merge and deploy code, you have released a tool that can be used. If you ship a gibberish math proof, it's not useful unless someone else can understand and deploy it to some other means. Now, it's possible AI could understand and make use of the math proofs, even if we can't, which refutes some of my hair splitting :)
- 318274 21d agoSo he got exuberant because he is funded by SAIR and the "AI for math" fund. And embarrassingly they used him for a "coal miners should learn math" moment that just benefits the AI industry. He has severely reversed course in the past week. Without concrete propositions it remains to be seen how much of the new resistance is for show.
- SavageNoble 21d agoI have zero formal math training beyond my Grade 12 Pre-Calculus class. Yet with an LLM I have recently devised an architecture with incredible math potential. Math is a language like any other, and without LLM's I never would have developed the techniques that I have. AI is a tool. It speaks languages I don't (Math, Science, Code). I would love to participate in a Math competition without a hint of any formal advanced math training because my experience so far tells me I will do well.
- breezybottom 21d agoHow could you possibly know if it has potential or not? Sounds like AI psychosis setting in.
- SavageNoble 21d agoBecause every test I run with it is telling me so? The great thing about math is it can be externally validated.
- BlackFingolfin 21d agoWho makes the tests? Who runs the tests? And who evaluates that the tests have meaning? As long as it is the AI, or you (with your self-admitted limited experience), how can you be sure it is meaningful?
- 8n4vidtmkvmk 20d agoYeah, but you're missing a gut intuition if something is off. I wrote a fancy polygon decomposition algorithm in university (pre-AI) which my professor didn't seem very impressed by because it was missing some sort of mathematical rigor. Yet everything I threw at it worked! Even he couldn't find a counter example. It took a while for me to find some failing cases but it turned out they did exist. But hey, maybe all I was missing is an AI-written lean proof.
- bobanrocky 21d ago‘Incredible math potential’ .. Yeah right, your AI said so ?!
- throw567643u8 21d ago>Dr. Tao Professor Tao.
- tzumaoli 21d agoIs this the scenario described in Ted Chiang's short story https://en.wikipedia.org/wiki/The_Evolution_of_Human_Science https://en.wikipedia.org/wiki/The_Evolution_of_Human_Science where scientists are "catching crumbs from the table" trying to decipher the results generated by superhuman intelligence?
- alkyon 21d agoIt's still an optimistic scenario. Artificial superintelligence may develop hypermathematics of a kind that never will be accesible to human mind, enhanced or not. One can't teach geometry to ants even if you put them on a Moebius strip. It would be more like Lem's novel where it completely disappears from the human horizon: https://en.wikipedia.org/wiki/Golem_XIV https://en.wikipedia.org/wiki/Golem_XIV
- GPerson 21d agoWhat’s optimistic or non-optimistic specifically about the machine having a system of mathematics beyond our comprehension within it? Why should we care about that in itself?
- alkyon 21d agoIn the first case, we'd still have a chance to take a glance at the frontier of discovery (even if ordinary human mathematicians had to spent years translating what metahumans achieved). In the second case all human-level maths would be solved and what lies beyond would be always out of our scope.
- genxy 21d agoWhich is why if humanity had empathy, it would be working on how to make smarter ants, so that they can learn more advanced geometry.
- CamperBob2 21d agoWhat do you think we're doing?!
- well_ackshually 21d agoSo it wasted everyone's time, thousands of hours of research trying to disprove something said very loudly. What OpenAI is doing is a DoS of the scientific community: wasting your time trying to check if they're not wrong, and claiming glory in the mean time.
- ksoped 21d agoAgreed! Although, if done by a mathematician, it's not a ~complete waste. I think the community learns something along the way. Is there an established term for the idea of "DoS"? I've taken to calling it slop fatigue.
- SJMG 21d agoDenial of service is the established term. Hammering their API (reviewer committees) would be an informal one
- tmhn2 21d agoThat's true, but the story would have unfolded differently if Mochizuki had a lean-verified proof and was correct. I guess baked into my premise is that AI is producing reliable proofs (in the long term at least).
- charcircuit 21d agoOpenAI avoids this by formally verifying the proof. https://github.com/openai/NavierStokesAndEuler https://github.com/openai/NavierStokesAndEuler
- well_ackshually 21d agoIt doesn't. It's 32 millions lines of bullshit, and the only thing it brought is "it's not true in some extreme conditions lol". The effort needed to figure out why that is, what conditions lead to it, the new mathematics that would need to be developed to solve their problem is once again being hoisted on actual humans, who now need to waste their time sifting through their slop.
- stabbles 21d agoThe maths community is now in the antithesis phase, synthesis will take a while ;) Lee Sedol said in an interview that "losing to AI, in a sense, meant my entire world was collapsing. ... I could no longer enjoy the game. So I retired", and I think there will be folks in the mathematical community who would feel the same when the solutions pages to hard problems are suddenly available. But on the other hand, people learned a lot from chess engines. After decades of chess computers beating humans, there was still a renewed interest in watching Leela beat Stockfish, with many people trying to understand the strategy Leela used. If your happiness comes from grinding on a problem and making progress, the prospect of having to dig through a corpus of AI-generated proofs might be hard to swallow. But if you're willing to do that, you will still find beautiful things that only so many people can truly appreciate.
- 318274 21d agoChess is kept afloat by a couple of billionaires like Sinquefield, MBS and the guy who sponsors freestyle (Fisher random) chess. Carlsen is bored by studying engine lines. The popularity is boosted by YouTubers because chess is very suitable for somewhat higher class content. I'm not sure we'd want that world for math. Positions will be cut just like archaeologist positions are cut now.
- mna_ 21d agoChess is kept afloat by chess players, not by billionaires. If all the billionaire backers stopped sponsoring tournaments, people like me would still play, still pay for chess club memberships, still pay entry fees for tournaments, and still buy chess books, and so on.
- debatem1 21d agoAlso, you learn to be a better chess player by... playing better players. The widespread availability of chess engines has made flawless opponents available to every player. If your goals are understanding the game, self improvement, building thinking skills-- this is the best chess has ever been. It's only if your goal is to beat every opponent you can find that chess is in a bad place.
- ksoped 21d agoIt's not just the isolated dumping, it's the fast, isolated, possibly untraceable dumping, without long term support. It'll basically become slop fatigue if OpenAI starts dumping out proofs faster than the community can keep up, and some turn out to be wrong, never formalize it, don't stay to support it, etc.
- tmhn2 21d agoI wonder if they will continue to dump proofs, though? Their point has been made, the novelty will wear off, and it maybe won't be a priority use of their resources to spend however many millions on another big proof--they will move on to the next thing to show off I'm sure. At that point, the ones generating proofs will be, I hope, mathematicians (professional and otherwise) that are more interested in the results and community discussion. (Well that's my hopeful, optimistic take, anyway.)
- famouswaffles 21d agoThey aren't going to stop at one, that's for sure. They already claimed they have "made substantial progress" on another millenium problem. Let's say they bag another one (Hodge and/or BSD according to the rumors), if it looks like their internal model could solve P/NP or Riemann Hypothesis, you think they wouldn't take that chance ?
- QuesnayJr 21d agoIf it's a counterexample to BSD, that would be pretty surprising. It would also be a considerably more impressive achievement, because experts had mostly shifted to Navier-Stokes regularity being false, while as far as I know almost everybody thinks BSD is true. Hodge people seem less sure about. If either conjecture is true and they prove it, that would be an even bigger success, since the techniques might unlock any number of other theorems.
- pizzly 21d agoI think AI companies making a point is not the only thing at play. Discovering new maths ultimately leads to new technologies and applications. It may start theoretically but end up being of practical use in the future. Even if humans do not understand it (lose interest, too complex, or just way too many new proofs to go though) AI can use this AI derived math corpus which will help it in other fields.
- deleted 21d ago[deleted]
- deanCommie 21d agoEven before AI we used to say if you write code that you only barely understand, then it will be to complicated to debug. (and/or maintain) Mochizuki was still one human and it required legions of other humans to unpack and untangle to confirm that it didn't lead to anywhere in particular. AI is now capable of constructions so complex that no human or human team can unpack. And its ability to increase that complexity is growing while our human ability is stagnant. meta-AI analysis cannot help. We (software professionals who use AI regularly) already know that if you run into a situation where a Fable/Astra-generated analysis reaches the limits of our comprehension/complexity due to their subjectivity, throwing more AI at the problem doesn't always converge. There are many reasons to feel optimistic about AI, and ultimately its general ability to help science and mathematics. I see no reason to feel optimistic about the future of mathematics and AI based on the current path of frontier labs, unless the misalignment Tao is writing about can be reconciled.
- zozbot234 21d ago> AI is now capable of constructions so complex that no human or human team can unpack. How can we possibly know this when we haven't even seriously started on the endeavor of actively reverse engineering these AI-generated proofs? That's a proper job for human mathematicians, because the AIs themselves are demonstrably clueless about what steps in a proof are genuinely interesting and load-bearing from a human POV. This is evidence of a limitation in AIs' capabilities, not of any kind of misaligned behavior. The fact that Tao actually uses that term in his complaint is deeply disappointing.
- kfse 21d agoNot to mention, there are already (pre AI) machine-generated proofs that we've pretty much agreed not to try to explain fully, like the four-color theorem which ends up with brute-force verification of 600+ cases (down from close to 2,000 when first demonstrated)
- 12_throw_away 21d ago> there are already (pre AI) machine-generated proofs that we've pretty much agreed not to try to explain fully, like the four-color theorem Algorithmic verification is a very unsatisfying answer to the problem (e.g., surely it's not just dumb luck that every single case happen to have this exact property), but that's an entirely different issue than saying that no one follows logic of the proof method itself.
- matco11 21d agoI get excited at the idea of a world in which advanced mathematical problems (and their solutions) become much more accessible to a much greater number of people. As a result, making mathematics much more loved at a societal level. Imagine a world where these most complex mathematical problems are not accessible to a few hundred people, but a few hundred thousands people. ...Those original few hundred gifted mathematicians would have an even more prominent role, and their names and achievements would be known by orders of magnitude more people that they are now.
- sghiassy 21d agoAs a laymen, I wish the same. But I also hope it doesn’t disincentivize those that dedicated themselves to the study
- genxy 21d agoMath department administrators fire Terence Tao. Based on current reward models, the frontier AI labs will burn down mathematics as an impressive display of capabilities and in doing so, will make it impossible for people that get paid to do mathematics to stay employed. If your job is literally to publish papers, and OpenAI and Anthropic decide that making an infinite-paper-printing machine is the best thing to show how effective their tech is, then as a demo, they destroy that industry.
- DoctorOetker 21d agoI wouldn't expect them to destroy that industry, imagine global squadrons of academics and mathematicians focusing their attention on LLM's, training algorithms, scaling laws, ... they're gonna try and beat the incumbent frontier AI labs, eye for an eye, tooth for a tooth
- genxy 21d agoThe apocalypse being triggered by frontier labs picking a fight with mathematicians was unexpected.
- onetimeusename 21d agoBut the work the Mochizuki case generated can also be done by AI. AI could generate a landmark proof and then people could use it to solve or simplify intermediate problems and you could use a different AI prompt to try to disprove it if you were really skeptical. From my memory I think they said it took 88 hours to solve a Millenium Problem versus the decades of time humans have put into it. I don't like nuance here. I think progress is really measured by what humans are able to do and understand, not machines. It is significant if we find problems we struggle to solve. That tells us something. What does it take for humans to solve these problems is related. The best analogy I can give is if you wanted to climb Mt. Everest you might ask someone for guidance. Would it be better to ask someone who has climbed Mt. Everest or someone who took a helicopter ride up near the top and then went to the peak? This is like the AI versus human gap to me. The helicopter is like using AI to generate a proof. The person who actually climbed Mt. Everest has firsthand knowledge of the experience. Same thing for a difficult proof. The struggle people have is actually valuable here. Likewise, we know people are actually capable of climbing Mt. Everest but if they had only ever rode a helicopter to the top, the knowledge of climbing it would not exist, and surely that is meaningful knowledge given the risks. So if we rely on AI for proofs I think we lose a sense of what is difficult and why. We lose a sense of what human achievement is. Surely climbing Mt. Everest means more than taking a helicopter up? For students, why bother grinding through all the material of climbing Mt. Everest and then attempting it if the helicopter ride is how things are done now? This would have the affect of destroying knowledge. (please do not nitpick the analogy because it's the best but perhaps a clumsy way to describe my thoughts)
- visarga 21d ago> Would it be better to ask someone who has climbed Mt. Everest or someone who took a helicopter ride up near the top and then went to the peak? Depends on if I want to go by helicopter myself.
- NateEag 21d agoTangent: > From my memory I think they said it took 88 hours to solve a Millenium Problem versus the decades of time humans have put into it. Keep in mind those ~88 hours were spread across ~10,000 simultaneous agent instances. So, roughly 880,000 hours of compute. Assuming a fifty-year career, and forty-hour workweeks, a human mathematician's career is about 100,000 hours of "compute". I suspect that with six good mathematicians spending their whole careers primarily focused on it, and working together closely, Navier-Stokes might well have fallen already. The perverse incentives of academia mean this has never occurred. The perverse incentives of industry mean OpenAI intentionally scooped researchers who were getting close (granted, with AI help). I'm not trying to dismiss the achievement - if the proof turns out to be solid, it's quite impressive (though much less so if the training data included the recent human breakthrough, which seems pretty plausible). I'm just pointing out that "88 hours" is a very misleading way of framing this.
- cevi 21d agoMochizuki's claimed proof of the abc conjecture was extremely unusual for the reason that nobody was able to extract a single useful idea from the argument. I was starting grad school when it came out, and my immediate visceral response was "if this is what number theory is going to look like in the future, then I will leave mathematics." The current wave of AI slop mathematics might end up driving the next generation of mathematicians away from the subject for the same reason that Mochizuki would have convinced me to quit if his proof had been accepted by the community. Luckily, my professors had the taste to immediately recognize that it was garbage.
- zahlman 21d ago> Ultimately we think a fatal flaw was found in Mochizuki's proof, so it didn't lead anywhere in particular. But in our hypothetical "AI lean-verified proof of RH" situation, it would presumably generate substantially more of that community activity we saw in the Mochizuki situation. And if it's correct, that community activity would be productive (expository talks, students given problems to flesh out or generalize, etc). This also sounds like a vector for trolling the community with complex putative proofs hiding a known flaw.
- amelius 21d agoNot if it's lean-verified.
- bayindirh 21d agoDidn't some of the recent proofs exploited a couple of blind spots of lean, and they were invalidated? Edit: Yup. A bug report to Lean was disguised as a "Collatz" proof in a humorous way. Links below. - https://x.com/gro_tsen/status/2082483878480977959 https://x.com/gro_tsen/status/2082483878480977959 - https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943
- fph 21d ago> Maybe mathematics just becomes a little more like other fields--relying on labs with lots of money for compute, digging through a corpus of AI-generated proofs, etc. I think a better comparison is: mathematics just becomes like mining bitcoins.
- sweezyjeezy 21d agoI think you might have to explain that comparison a bit more to be honest. How are math proofs like bitcoins? A bitcoin has a pre-defined value, a math conjecture / proof is a bit more complicated.
- roywiggins 21d agoIf there's a machine that automatically turns electricity into proofs then mathematics becomes a different thing altogether.
- Timwi 21d agoA Bitcoin does not have any pre-defined value. The value of Bitcoin keeps fluctuating, and historically has risen dramatically from its initial value of 0. If this weren't the case, there would be no investment/speculation in Bitcoin because there would be no potential for any ROI. In reality, the value of Bitcoin is determined by humans (even if indirectly, not by planning), and I think the OP’s point may have been that maths proofs can be regarded similarly. No intrinsic value, just what humans find in it.
- citizenpaul 21d agoI've met a few Ph.D Mathematicians in Academia socially. My unfortunate experience was that they were insufferable,borderline hostile people. I tried to genuinely engage with them too. I've met one Ph.D Mathematician that left the industry whom was very enjoyable to talk to. I have a feeling that my experience was not unique and the Math world is mostly a bunch of too good for everyone on their high horse a-holes that are now being knocked down a peg. They don't like it obviously. I'm not a fan of knocking down things that work, however I also find it hard to be against death of the gatekeeping old guard of any industry. I think math is just gonna have to suck it up like every other industry now. Math productivity is longer out of reach of the average grad student. Like every other industry they are no longer untouchable and are gonna have to adjust to the new way of things or market forces will do what they always do which is refuse to fund ineffectiveness. I've had to accept that tech/IT will never be the same. Just how it is. You can thrash against it all you want.
- kzz102 21d agoThe difference is the scale. A few incomprehensible long papers per year, sure, we will study it. A flood of AI results closing research directions left and right, that will be a problem.
- embedding-shape 21d ago> closing research directions left and right Why would research be closed in one direction? Even if AI or human says "Tried that, didn't work" or whatever, someone (or something I suppose) might very well retry it in the future, if nothing else to reproduce it didn't work, in theory at least.
- kzz102 21d agoAI tends to take nearly finished research directions and push it to the conclusion in one step. If deployed massively, it will pluck all the low hanging fruits causing a drought of near term promising research project. Because people who start promising research directions do not get to see it finish, over the long term fewer people will start new directions, causing the field to slowly whither.
- _superposition_ 21d agoI really like this take, and while I hate math I value it. Your position sounds extremely plausible and it fits with the pattern we see in the community here. Regardless if it's ai slop or not we still debate the value and attempt to understand. In the process generating new insights and ideas. Life will go on.
- deleted 21d ago[deleted]
- GPerson 21d agoIt’s frustrating that this comment is at the top because it, along with lots of the replies it inspired, absolutely misrepresents the actual declaration. The declaration is not making any statements about not using any AI in mathematics. The entire point is to push the use of the technology in a direction which is compatible with positive pre-existing features of the math community, and to make it better known what some of the current problems are.
- qlte 21d agoIt includes Terrance Tao who has made the front page several dozen times at this point for his usage of AI such as to help the community write proofs for Erdos problems. But to many commentors he's a now gatekeeping AI-hating Luddite clinging to a dying profession out of bitterness and envy because his position is more nuanced than "throw AI at everything and turn off your brain".
- deleted 21d ago[deleted]
- zozbot234 21d agoBecause his letter misuses the word "misalignment" for what's very clearly a capability gap. To anyone familiar with that sort of language, his prose is directly implying that evil superintelligent AIs are deliberately writing obscure proofs in order to harm the community of human mathematicians, which is exactly what the AI-hating Luddite would say! The reality is closer to "current frontier AIs are clueless about what makes mathematical problems/proofs interesting to humans" which is a vastly different issue.
- necklesspen 21d agoLLMs are tools. The responsibility lies in the human(s) using the tool to act accordingly.
- jhrmnn 21d agoIt’s actually a fairly precise use of the word, just not in the very specific and narrow sense in which it has been used for AI.
- MurkyManzarek 21d agoThis comment represents the situation around Mochizuki's "proof" completely wrong. Yes, there was a lot of activity around 2012 (seminars, workshops etc.), but it was all wasted effort. No interesting mathematical ideas and tangents came out of it because the proof was just garbage, as conclusively etablished by Scholze & Stix in 2018. So Mochizuki's proof ended up in hundreds of hours of work wasted on nonsense. I don't think this is the type of community engagement that Tao and others have in mind.
- vitriol83 21d agoBut Mochizuki didn't actually prove anything, whereas the labs have already done so. The pessimistic scenario is the AI labs will continuously hoover up new developments in mathematics and gazump everyone in their respective fields. It's clear they have no desire to participate in any silly academic niceties, like properly assigning credit or expository work for normal humans. What incentive then do humans have to do this work ? Generally the mood amongst research mathematicians is pretty dire, and I don't really blame them. To be clear I think AI is super useful for mathematical research, the problem is the methods of the big labs are massively disincentivising mathematicians from engaging in research, and other associated tasks like giving seminar, teaching writing books etc. These arguably have much more value than finding an obscure counter example to Navier-Stokes.
- rossant 21d agoI agree. What would stop the AI from explaining the proof in a way human mathematicians can understand, and then giving them a roadmap for spreading it through the community via textbooks, conferences, and so on?
- breezybottom 21d agoHow do you write a grant for that though? "I plan to prompt Claude until it eventually spits out an answer"?