| ▲ | shubhamjain 7 hours ago |
| A very balanced perspective, and the concerns he raises are reasonable. He acknowledges that AI is going to transform mathematics, but simply dumping proofs on the math community and expecting others to do the grunt work of verifying, refining, and expanding on them is hardly a productive way to advance the field. There seems to be more interest in hitting some arbitrary benchmark (we proved X unsolved problems) than in genuinely contributing to mathematics. But what else is to be expected? It's become a maniacal race with too much money. Too much effort is being invested in proving that the exponential curve is still holding. |
|
| ▲ | kuboble 5 hours ago | parent | next [-] |
| I wonder if top labs will soon abandon math progress like they did go and chess. In example of go where I'm more familiar Google deep mind poured large resources to get a super human performance first, establish superiority and abandon it. The community then built their own tools starting from reproducing their papers. I think similar thing might happen to math. Nobody outside of math cares too much about Hamiltonian cycles in some bizarre graphs or proving lower bounds on complexity of some problem. Once those results stop being worthy of mainstream media attention, they will abandon math and the progress will be done by mathemicians guiding the models and the community will likely establish some new rules about what makes a valuable contribution. Merely solving not yet solved problem might not be it anymore. |
| |
| ▲ | curt15 2 hours ago | parent | next [-] | | The amount of money they're lately ploughing into proving math theorems is inconsistent with how societies and markets have priced pure mathematics. The entire US federal budget for math research is something like $100M annually. A single college football coach can already earn 10 percent of that. Pretty much the only enterprise that historically pays some mathematicians handsomely is quant finance, but those people are actually compensated not for proving theorems but rather for statistical modeling and programming skills. And even that industry is so technologically driven these days that pure research mathematicians no longer hold a clear edge over strong programmers with undergrad level probability and statistics at their fingertips. | | |
| ▲ | dannyw an hour ago | parent | next [-] | | Math is one of the most verifiable domains, esp thanks to LEAN, which also build coding skills. The $$$ they're pouring isn't just for marketing. Think of these papers/results more as "useful side effects" from large-scale RL rollouts and post-training. Every token being generated contributes to post-training in some way. There isn't a hard boundary between "training" or "inference", modern post-training is arguably inference-bound :) | | |
| ▲ | bonoboTP 41 minutes ago | parent [-] | | It was shown quite some time ago that training LLMs on programming tasks improves their logical reasoning skills also in other natural language domains. So I could see math also being a training gym for AI even if the final use case is not directly math-related. Having to solve math problems efficiently can build in skills that come handy in all kinds of more everyday tasks or science and engineering. |
| |
| ▲ | jeremyjh an hour ago | parent | prev | next [-] | | As long as they continue making headlines they will continue spending. This is just marketing at this point. | |
| ▲ | ogogmad an hour ago | parent | prev [-] | | Don't hire a straight-A student, unless it's to take exams; or a professor, unless it's to write papers.
-- Nassim Taleb
How interesting that Anthropic and OpenAI are full of professors and straight-A students! | | |
| |
| ▲ | Xmd5a 4 hours ago | parent | prev | next [-] | | I don't think it will be the case, maths have real utility. I found something interesting at the intersection of combinatorics and information geometry. To be quite frank I don't understand what I'm doing. And yet, when I ask ChatGPT to use the framework we're developing to write an algorithm, it turns out it has quasi-parity with the state of the art. I have to measure absolute perfs to decide which one is better – theirs, not mine. Ok. Time to keep improving on what I have. And this implies dropping the code and going back to the blackboard doing more super abstract math that are way out of my league. | | |
| ▲ | lh712 3 hours ago | parent | next [-] | | Good luck! We are at the point where the way in which humans do math and science changes significantly, and I have no good idea at all in what state is it going to settle down. But you are one of (many, I suppose) people exploring the new wilderness, so I wish you best. | | |
| ▲ | Xirdus 41 minutes ago | parent [-] | | If we get AI singularity, then humans will stop doing scientific progress altogether. But if we don't, then it's pretty predictable what's going to happen - things will be much the same as now, except everyone will be using AI for proofs, data analysis, theoretical models and designing experiments, so important discoveries will happen more often. It's also possible that after the AI craze dies down, we'll have enough computational capacity to solve protein folding. |
| |
| ▲ | kuboble 2 hours ago | parent | prev [-] | | It has utility so some people will pursue it, but it has no immediate business value so I don't believe ai labs will keep spending millions on it. Unless they decide that trying p!=np is worth any money. | | |
| ▲ | dannyw an hour ago | parent | next [-] | | Why do you think this has no business value? It would be absolutely wasteful for OpenAI to not be doing this as part of a post-training RL rollout. There are architectural advancements yes, but lots of progress from LLMs really come from (1) better pre-training [generally through more cleaned data, and ofc more data], and (2) lots and lots of post-training. It's how we get more and more intelligent models for the same param sizes. The 'marketing' is just a useful side effect they get from their RL rollouts on maths and LEAN. | |
| ▲ | TheOtherHobbes 2 hours ago | parent | prev | next [-] | | Some math has almost incalculable business value, because math is the biggest driver of game-changer technology. We'd be nowhere without Laplace and Fourier transforms, Maxwell's equations, elliptic curve cryptography, and many more. Most math doesn't, but often these techniques are invented first and the applications come later. And the criticism of the current round of proofs is that while they may be true - likely for some, questionable for others - they're not adding new techniques or insights. | | | |
| ▲ | IanCal 2 hours ago | parent | prev [-] | | There is a risk of this particularly if it's seen as advertising - at some point "ai model solves hard to explain problem" isn't going to be news and that benefit goes. However, there's some of this that's a proxy - the compute to solve these problems was very low (they claim a few hours of thinking time on a regular subscription). The large cost would have been the training and if training the models to be better at these things makes them smarter for useful tasks that's beneficial. I believe there was work done earlier on around showing that training the models on code made them better at broader reasoning tasks (not just writing the code itself). Another side is that if one goal is to improve the models themselves, their ability to work on mathsy problems must be high. That has very direct business value, and ideological value depending on what you think the motivations of the people running the companies are. |
|
| |
| ▲ | mohamedkoubaa 7 minutes ago | parent | prev | next [-] | | They already proved the point | |
| ▲ | pizza234 4 hours ago | parent | prev | next [-] | | > I wonder if top labs will soon abandon math progress like they did go and chess. I definitely think that this is marketing, just "with good side effects". My doubt is when they will be able to move to "marketing with better side effects", that is, research with more concrete outcomes (health, materials etc.). Problem is, that type of research is much harder. Some doubt that progress in such areas will be quick (https://www.noahpinion.blog/p/wheres-the-intelligence-explos...). | | |
| ▲ | simonh 2 hours ago | parent | next [-] | | They aren't trying to 'solve' chess, go, or mathematical proofs as an end in themselves, but mainly in order to learn more about how to build better systems overall. The goal of AlphaZero was ultimately as a stepping stone towards AGI, and it's the same with LLMs. | | |
| ▲ | catlifeonmars 2 hours ago | parent [-] | | The assumption being that
1. these things are all stepping stones, not diversions
2. that ai labs have a singular goal of producing agi |
| |
| ▲ | td6 3 hours ago | parent | prev [-] | | Would that be a bad thing? While top AI labs no longer focus on chess, the community build way better chess engines. Stockfish is probably stronger, than everything the top labs build. Wouldn't we expect the same thing for math? That slowly the broader math community would engineer a harness/program... That will surpass the current labs, and be a community ran project | | |
| ▲ | sebzim4500 3 hours ago | parent [-] | | Yeah its certainly true now that Stockfish is much stronger than alphazero, but it's probably also true that had Deepmind spent another few years working on alphazero it would be enormously stronger than either. In the case of chess this seems fine, there isn't much value to society in creating an AI capable of beating top humans with a 4 pawn handicap rather than a 2 pawn one, but for maths where there are actual applications it is more complicated. | | |
| ▲ | kuboble 28 minutes ago | parent [-] | | But arguably - it's better for chess community that the best engines are opensource than having superior GoogleChessBot. |
|
|
| |
| ▲ | squidbeak 2 hours ago | parent | prev | next [-] | | AlphaGo and AlphaZero weren't generalized models. Math capability will presumably keep improving along with the other general capabilities, even if there wasn't a special RL focus for math itself. | |
| ▲ | diamondage 5 hours ago | parent | prev | next [-] | | This misses the raw advantage of a good proof. It makes conceptualization simpler. In some ways math is like a hash list of of theorems. This list makes it simpler to prove other calculations, and will always be useful, to both humans and AI models. I can see two new directions 1 - the creation of specialist theorem models; that can answer questions efficiently about one topic and 2 - we probably need to incentivize and codify ownership of theorems; charging a proportion of the compute saved by using them. Ultimately enabling mathematicians to be paid our true market value! | | |
| ▲ | edot 5 hours ago | parent | next [-] | | Oh boy, please not 2. What if this was a thing already and, since neither Newton nor Liebnitz had kids, we all had to pay some investors who bought the rights to calculus every time we took a derivative. | | | |
| ▲ | lh712 3 hours ago | parent | prev | next [-] | | Considering how essential math and science is for the prosperity of mankind (not even speaking about the cultural value) the question of how to reward people working and contributing in these fields effectively and appropriately is of extreme importance. (And I think the current decline in our societies is to no small degree caused also by our utter failure to address that issue.) It is also fascinating, because I don't think there is any solution within our existing system, at least not any I know of. Theorem ownership is not a good solution (and neither are patents in general). Probably the most achievable (or rather the least unachievable) solution is a kind of communist utopia, where people can dedicate their time to a pursuit of any endeavor they see fit, as resources for a decent life are abundant and excessive power capture impossible. (The other option, somewhat dystopian, and which would not require humanity to change too much in its current mode of conduct, would be a totalitarian or caste-like capture of society by the scientific community.) Incidentally, if AI proves as powerful as some expect it to become, it could bring about another solution of that issue by making all human science and mathematics obsolete, pushing its true market value to zero. (With apologies for rambling.) | |
| ▲ | petesergeant 3 hours ago | parent | prev [-] | | > It makes conceptualization simpler I wonder if it makes conceptualization simpler for models too, given that they're trained already on human-speak. And I'm also curious as to whether humans currently have an innate advantage into simplifying and contextualizing proofs, or will the machines get good at that as well? |
| |
| ▲ | renyicircle 4 hours ago | parent | prev | next [-] | | I had the same idea recently. You've solved all the famous conjectures (all formulated by humans because humans found them interesting), what next? I doubt "AI formulated a math conjecture that nobody else cares about and immediately solved it" will produce that much hype. The actually interesting thing is indeed how mathematicians themselves will use these AI models going forward and how that will shape mathematics of the future. | |
| ▲ | bluecalm 4 hours ago | parent | prev | next [-] | | Yeah chess is a good example. DeepMind came for publicity with AlphaZero. Arranged a match with Stockfish with rigged rules to make AlphaZero look better than it really was (it was amazing but the match wasn't fair) and then just published some games and went home. I was bitter about that back in the day as I hoped for more answers, more matches, more "truth" about chess being shown. Soon after that community project Leela Chess Zero was started and not only surpassed original AlphaZero but added few hundred ELO points over it. Then the combination of NN and classical engines happened with NNUE and current Stockfish is again a few hundred ELO points stronger. Today we pretty much know the truth in chess for all practical purposes. Human analysts/preparation experts focus on finding interesting path and opponent profiling (what is the most unpleasant for the opponent to face). They don't look for truth anymore. The game is doing great, it's more popular than it ever was. | | |
| ▲ | squidbeak 2 hours ago | parent [-] | | Why don't you mention the second match here, with its adjustments to meet Stockfish's quibbles - and the same result? https://en.chessbase.com/post/the-full-alphazero-paper-is-pu... | | |
| ▲ | bluecalm 2 hours ago | parent [-] | | Stockfish and other classical engines were never intended to be run in matches without opening books (of which there were plenty).
Development assumed the presence of opening book and authors made 0 effort to make engines play well in openings because of it.
This is also the reason classical Stockfish was a very small binary. A little effort to make it even by including even a very small opening book (like 50MB or something that would result in still smaller binary than NN engine with its net) would make it much more interesting. The result was that Stockfish lost many games by walking into known bad lines and lost way more games than it otherwise would. | | |
| ▲ | squidbeak an hour ago | parent [-] | | You aren't correct. > We also played a match that started from the set of opening positions used in the 2016 TCEC world championship, along with a series of additional matches against the most recent development version of Stockfish, and a variant of Stockfish that uses a strong opening book. In all matches, AlphaZero won. https://deepmind.google/blog/alphazero-shedding-new-light-on... |
|
|
| |
| ▲ | im3w1l 4 hours ago | parent | prev | next [-] | | I disagree. Firstly, people in AI likely care about math on a personal level. Secondly math is useful. Playing go or chess is basically a party trick. Being useful gives it staying power. But, I do think you are right that there will be some level of moving on. The spotlight is currently on maths and that won't last. It will move to some other area where there is more impact to be had. So while they might shift gears and put less focus on math, it will always be there as part of the portfolio. | |
| ▲ | techpression 2 hours ago | parent | prev [-] | | I think there’s a venue where they start focusing on introducing hypotheses where the model currently can’t solve it, or maybe this is already happening? Being able to present useful novel ideas would likely generate a lot of press, for a while. I don’t know how this would look since I’m useless at math, but Im sure there are plenty of unknown problems with massive implications, that once formulated can be solved. |
|
|
| ▲ | antman 6 hours ago | parent | prev | next [-] |
| This argument implicitly makes a few assumptions which will probably not hold in the very near future. One is that AI will continue hallucinating in a manner that is not easy to verify, second is that AI will not be enhanced to produced more simplified amd robust outputs, and third that a human will be required to do that.
What humans in the loop are doing now is verify the process, propose shortcuts and add legitimacy, through the verification process, if that ends up being succesful its highly likely a lot less mathematicians will be required in the future. The conclusion that this is not productive focuses on the mathematicians, but it is very productive in terms of hundreds of proofs being produced that had previously consumed uncountable hours of the brightest minds. Unless it ends up being the greatest hallucination ever ofcourse |
| |
| ▲ | Vetch 5 hours ago | parent | next [-] | | Putting hallucination aside, LLM "theory of mind" has gotten worse over time. I feel it peaked in Opus 3 and Sonnet 3.5, GPT 4 and then GPT 4.5 for OpenAI. Since then, even with Opus 5.5, phrasing has needed careful crafting, in order that it not be taken too literally. OpenAI models suffer from this much more than Anthropic models but Claudes have backslid over time too. This means when writing documentation, tutorials or commit messages, their output is often a garbled jumble. Assuming shared context, using invented terminology without explaining, leaking conversational states due to improper epistemic boundaries and failing to model the reader. This all usually leads to their freely generated explanations being terrible. Getting good explanations requires chaining questions that force them to line things up properly, which is not easy the less you know. These failures as something LLMs naturally struggle with make sense, given the nature of attention and RL with weak signals from human data. Math is not merely a collection of proofs, it's a way of understanding. A proof presented in a manner that cannot be incorporated remains useless. It does not make it's way to physics like Riemannian geometry and matrix math did. This is no less true when done by humans too. Your hallucination conclusion, checking if a proof is one, is exactly the counterproductive cost. Most of us cannot verify that the claims in the OpenAI lore dump are in fact all correct. It will take tons of work from experts to do this. It took subject expert mathematicians to identify the discrepancy and disconnect in the Navier Stokes proofs, for example. LLMs will struggle to make use of their own proofs or turn them into knowledge that accumulates over time. The act of proving is often more valuable than the proof itself. Human constraints and limitations force us to invent tools and abstractions that a 100,000 x 1M context swarm can bypass. The tradeoff from that AI swarm advantage is work that doesn't usually lend itself to being built upon. It's like doing all the side quests and reading all the books of an RPG versus min maxing a straight path with a guide. We might try to identify new abstractions, but the fact that we don't get access to CoT and that much of it will be illegible means mining LLM traces for what human mathematicians produce naturally will be a tedious chore. | | |
| ▲ | p-e-w 3 hours ago | parent [-] | | > Since then, even with Opus 5.5, phrasing has needed careful crafting, in order that it not be taken too literally. This is a feature, and a huge step forward. If you expect AI to do serious work, you can’t have it guessing what you “really meant”. Every sufficiently advanced task depends on very subtle details in the problem statement, and the correct default behavior for advanced AIs is to solve the task exactly as stated, unless a system prompt or other constraint tells it to do otherwise. |
| |
| ▲ | dofm 5 hours ago | parent | prev | next [-] | | > One is that AI will continue hallucinating in a manner that is not easy to verify It is an old saw at this point, but what an LLM does still cannot be divided into hallucination and non-hallucination. This is literally an anthropomorphism trap. Layers and layers of application-specific verification can reduce the risks inherent to LLMs, to a really remarkable degree, but nothing about what these tools are suggests that this problem will go away; it will just bubble up again somewhere else. | | |
| ▲ | user43928 4 hours ago | parent | next [-] | | And why not? For all that I saw over the last few hundred hours with AI on software engineering, hallucinations are no longer a problem at all. Not once have I seen a task fail due to what would have been a "hallucination". If they still occur, they can apparently be detected and corrected automatically, or are subtle enough to escape notice with presumably no significant impact on the results. Why would this not also be the case for mathematics? | | |
| ▲ | catlifeonmars an hour ago | parent [-] | | I think OP is saying that hallucination or not is just semantics. There is nothing qualitatively different about hallucinated vs non-hallucinated output. | | |
| ▲ | bonoboTP 32 minutes ago | parent [-] | | That's true in the same sense as "There is nothing qualitatively different about erroneous vs non-erroneous output" for a dog vs. cat image classifier. | | |
| ▲ | user43928 25 minutes ago | parent [-] | | To be fair, I guess the line is blurry between what could be labelled a regular mistake compared to a hallucination. "Test suite passed" when it actually errored? Obvious hallucination, unless it ran a command that returned the wrong error code. But is running a malformed command that does not achieve the expected effect itself a hallucination? |
|
|
| |
| ▲ | antonvs 5 hours ago | parent | prev [-] | | > It is an old saw at this point An old saw unless something that's widely accepted, but sadly it seems that many people don't recognize this, even many people working in the field. |
| |
| ▲ | Terr_ 6 hours ago | parent | prev | next [-] | | > assumptions which will probably not hold in the very near future [...] One is that AI will continue hallucinating in a manner that is not easy to verify Hold up, that's an even bigger assumption in the opposite direction, and I don't see anything to support it. At least in terms LLMs getting all the "AI" hype these days, there is no structural/mathematical reason to believe they won't continue to have the same problem they've always had of generating plausible text over rational text, and I don't think anybody even has a clear idea how it could eventually be accomplished. I've seen "then the magic singularity occurs and somehow it solves the problem for itself", but I would classify that more as mysticism than engineering. | | |
| ▲ | user43928 4 hours ago | parent | next [-] | | Hallucinations are no longer much of a practical problem in software engineering. Two years ago, hallucinating that the code worked or that a task was accomplished was a common occurrence. We have seen that now agent swarms across thousands of agents can coordinate to achieve a result. Clearly hallucinations are no longer the problem they once were, since now we can get working results for long horizon tasks that require massive compute. Consequently it would seem unwise to assume that current limitations will remain as they are and prevent LLMs from coming up with solutions that they can explain to humans. | | |
| ▲ | ashkankiani 43 minutes ago | parent | next [-] | | The confidence with which you, anonymous user, keep commenting that "hallucination is not much of a practical problem in software engineering anymore" based solely on your own anecdotal evidence is really remarkable, in not a good way. | | |
| ▲ | user43928 39 minutes ago | parent [-] | | You're free to substantiate your comment by telling us about your apparently different experience. | | |
| ▲ | ashkankiani 17 minutes ago | parent | next [-] | | The sum total of all human observations is still not proof of the lack of hallucinations as a problem (even if their observations were perfect, which they aren't considering the volume produced vs reviewed carefully). That's why you can use a counter example only to disprove and not prove anything. And yeah I get hallucinations all the time still. Maybe it's because I'm working on harder/more niche problems (like a compiler with an unusual type system), but it happens quite a lot. I don't record all of them. Although the most common one you can find is them misattributing the source of changes from themselves and also other agents (Fable, Opus 5.5, deepseek, whatever). They'll say "your changes" or "you changed" or "your ruling." I didn't decide anything and it's in their own chat log, and yet... | |
| ▲ | jazzypants 25 minutes ago | parent | prev [-] | | I find hallucinations in my (mostly perfect) AI output every single day. If you're not finding them, you're just not looking hard enough. It's not surprising when everyone is screaming about how they don't read code these days. This is just a fact. I'm sorry if it messes with your narrative. https://arxiv.org/abs/2401.11817 | | |
| ▲ | user43928 21 minutes ago | parent [-] | | Thanks for the link. What kind of hallucination are you seeing, and does it affect the end result? |
|
|
| |
| ▲ | catlifeonmars an hour ago | parent | prev [-] | | It’s still a common occurrence. It happens in more subtle ways, but it still happens often enough for me to notice. For example I have had hallucinated checksums show up in lock files as recently as yesterday using a SOTA model. This is not surprising, since the whole basis of LLM training is to produce output that humans will accept _as a proxy for actual training goals_. In a sense, the training process of an LLM “wants” to produce output that is statistically plausible much more than it “wants” to produce correct output. It’s always going to be a struggle to drive that system towards other goals (and we see this bourne out in practice by the amount of effort that is required to be spent on RL). I think there will be some threshold of correctness (something like 99.999% of the time) that if the model surpasses it, I can stop needing to check it, but I think we’re still at 99% or something which sounds good, but when you are producing a ton of output you hit that 1% frequently. > Consequently it would seem unwise to assume that current limitations will remain as they are and prevent LLMs from coming up with solutions that they can explain to humans. I 100% agree with this. In fact explaining things to humans is something LLMs are particularly well suited for. |
| |
| ▲ | hodgehog11 5 hours ago | parent | prev [-] | | "Plausible" text was preferred over rational text when we trained LLMs using RLHF. It's rapidly shifting the other way now with RLVR, which enforces correctness by default. |
| |
| ▲ | catlifeonmars an hour ago | parent | prev | next [-] | | > but it is very productive in terms of hundreds of proofs being produced that had previously consumed uncountable hours of the brightest minds You’re making the following assumptions: 1. the exercise of struggling to find proofs was not productive, but this is precisely how new techniques in math were produced. Brute forcing solutions doesn’t lend itself to the creation of much new mathematics (except maybe the exercise of developing verifiable proofs) 2. the point of doing mathematics is to be “productive” in the first place. This is silly. Many people get into mathematics because of the beauty of understanding, for example. | | |
| ▲ | bonoboTP 36 minutes ago | parent [-] | | > 2. the point of doing mathematics is to be “productive” in the first place. This is silly. Many people get into mathematics because of the beauty of understanding, for example. Are they independently wealthy? Or do they have a deal with their local supermarket that they can take food for free? |
| |
| ▲ | Retr0id 6 hours ago | parent | prev | next [-] | | Even if you somehow have a 100% correct AI, it's not useful unless we can understand and internalise (and communicate) its results. | | |
| ▲ | colordrops 5 hours ago | parent [-] | | Who is this "we" you speak of? The professional mathematician community? Were pre-AI results useful outside of this community of people who could understand them? | | |
| ▲ | hodgehog11 5 hours ago | parent | next [-] | | Yes. Most probably do not understand the notation involved in, and the statement of, the Lindeberg-Levy Central Limit Theorem. But every scientist uses this theorem in one way or another. These ideas have a way of trickling down because to people who work thanklessly to do so. | |
| ▲ | dofm 5 hours ago | parent | prev [-] | | Something about this sentence makes me think about that Rob Auton bit, that before there were mobile phones, nobody had any reason to tell someone else that they were on a bus. | | |
| ▲ | zer00eyz 2 hours ago | parent [-] | | Before mobile phones you never called someone and asked "where are you" because a phone was tied to a location... |
|
|
| |
| ▲ | mathisfun123 6 hours ago | parent | prev | next [-] | | > One is that AI will continue hallucinating in a manner that is not easy to verify, second is that AI will not be enhanced to produced more simplified amd robust outputs, and third that a human will be required to do that. There is literally not a single shred of evidence to indicate either of your supposed eventualities. The core technology of an LLM is sampling from a distribution so there is literally no way to make it deterministically robust (only probabilistically). | | |
| ▲ | bonoboTP 27 minutes ago | parent | next [-] | | Is a human deterministically robust? Or is a human also incapable of doing what you claim LLMs will never be able to do? | |
| ▲ | antman 5 hours ago | parent | prev | next [-] | | The direction and pace of capability improvement has already been demonstrated by all models. The latest breakthroughs make that pretty evident, but there have been production systems that are based on probability since the beginning of computing. What has been demonstrated is a process that outputs lean proofs based on those probabilities. This happened after decades markov chain producing garbled texts and very shortly after gpt2 producing stories about unicorns. | |
| ▲ | red75prime 5 hours ago | parent | prev [-] | | > The core technology of an LLM is sampling from a distribution so there is literally no way to make it deterministically robust (only probabilistically). An LLM mostly deterministically (except parallel processing nondeterminism that can be mitigated) produces a probability distribution that can be sampled deterministically: just take the highest probability token or use beam search. | | |
| ▲ | gottheUIblues 4 hours ago | parent | next [-] | | I think people on here tend to somewhat fixate on the determinism issue. Even with a deterministic LLM - stabilising the floating point arithmetic, and choosing from the distribution by a fixed method, or just save the random seeds - there is still a kind of a chaotic unpredictability that can exist between its inputs and outputs. However maybe that is a price that needs to be paid to get creativity. | |
| ▲ | Vetch 4 hours ago | parent | prev [-] | | Deterministic yes, robust deterministic no. The most likely conjunction is not always the best nor representative of what the model is considering unless its certainty is high. | | |
| ▲ | red75prime 3 hours ago | parent [-] | | I think determinism has nothing to do with it. If you mean sensitivity to word ordering and such, it's a generalization failure. |
|
|
| |
| ▲ | thereitgoes456 6 hours ago | parent | prev | next [-] | | AI cannot explain chess moves it comes up with in an elegant way. What makes you think it will be able to do so for math? | | |
| ▲ | ApolloFortyNine 2 minutes ago | parent | next [-] | | Interesting claim. That's true for old models that simply have no way to explain, LLMs however can. [1] [1] https://dev.to/natcher/researchers-develop-method-to-train-l... | |
| ▲ | jstummbillig 6 hours ago | parent | prev [-] | | It's kind of astonishing that after all we have seen in the last years people still find the position that AI will not be able to do an obviously valuable thing likely and it requiring an explanation (instead of the other way around). | | |
| ▲ | hodgehog11 6 hours ago | parent | next [-] | | No, this is different, and this is coming from someone who has been studying deep learning for the last decade. We are talking about the difference between RLHF and RLVR strategies. The former benefits clarity and explanation, while the latter concerns only correctness. AI was moving in a particularly damaging direction by pushing on the first path, so it was natural to move to the second. But the second will come at the cost of clarity of explanation. It will likely get better at its explanations, but not fast enough to render its most advanced accomplishments readily understandable to the user. The chess example is a pretty good one (that is an RLVR approach). | | |
| ▲ | __s 9 minutes ago | parent | next [-] | | tbf GM explaining their 2700 elo moves are only understandable when vague, as elo goes up explanation becomes closer to "in this specific position there's these dpecific lines", why should 3500 elo moves have simple reasoning? Maybe if we start with giving simple AI generated analysis of those clumsy humans with their measly 2700 elo moves | |
| ▲ | red75prime 5 hours ago | parent | prev [-] | | The problem is that people strongly believe that this is an insurmountable problem that will persist indefinitely (or for a long time) and plan accordingly, while this, most likely, will be fixed soon by adding RLCAF (RL on conversational agent feedback) or something like that. |
| |
| ▲ | n6242 5 hours ago | parent | prev [-] | | Some of us still remember 2016, when we had a couple of cars sorta half-driving themselves, and Tesla, Uber and others promised we were only one year or two away from three million people in the US working as drivers being out of a job. And here we are, a decade later. AI is pretty amazing, but companies have a tendency to severely and comically overestimate and oversell it's capabilities, and underestimate the challenges. | | |
| ▲ | jstummbillig 4 hours ago | parent | next [-] | | > And here we are, a decade later. With Waymo and Tesla increasingly doing what they said they would do, and a small number of early adopters happily paying money for their services, that do work. So what's the critique? That the timelines are not correct? Sure. And how about the timeline of the people who said "research level math, never in my lifetime" and the people inside the ai companies who are apparently increasingly spooked by how quick the progress is? How about the various levels of code/programming jobs that AI was supposedly never going to be able to do, but, in reality, now just does? We are engaging in some very one-sided discrediting, and I am not sure, why. | | | |
| ▲ | p-e-w 3 hours ago | parent | prev [-] | | Driving a car is unimaginably more difficult than proving the Riemann hypothesis. You just don’t notice that because evolution has given you 99% of what is needed to drive a car before you were even born. |
|
|
| |
| ▲ | nullsanity 6 hours ago | parent | prev | next [-] | | [dead] | |
| ▲ | wolvesechoes 5 hours ago | parent | prev | next [-] | | Expression of tech-faith is not intellectually honest argument. Where does this "will probably not hold in the very near future" come from? People correctly warn about extrapolating current things onto the future, but then just throw some vague "probabilities" without providing any argument why their "probably" is somehow more grounded than others. | | |
| ▲ | antman 5 hours ago | parent [-] | | Markov chains garbled text to gpt took decades, gpt stories about unicorns to gpt production systems took a few years, gpt production system to gpt astra producing deterministic lean proofs of longstanding mathematical problems happened even faster. Scepticism to the point of requiring proof appears like an academic pursuit while production systems have already been built and are in the process of being enhanced |
| |
| ▲ | pegasus 4 hours ago | parent | prev [-] | | Did you even RTFA? His argument absolutely doesn't make any assumptions about hallucinations, implicit or not. It's you who assumes Tao must have surely been complaining about hallucinations or some such. You've not addressed any of his arguments and moreover ask questions his post answers. Here's a longer article which goes into a bit more of the details: https://terrytao.wordpress.com/2026/10/05/the-future-of-math... |
|
|
| ▲ | charlieyu1 3 hours ago | parent | prev | next [-] |
| The biggest problem is LLM tends to produce over engineered, very complicated proofs that are an eyesore even for relatively simple problems. Give it a beautiful Olympiad geometry problem and LLM will tear it apart into ugly algebraic calculations, turns all lines and circles into equations and calculate their intersection points that spans multiple pages because it is a guaranteed way to solve it. Correct, but hardly any use to the user. |
| |
| ▲ | Gigachad 2 hours ago | parent | next [-] | | I’m not deep in to math but the op tweets make sense to me. In that it’s not just the final proof that mattered, but the mind and understanding of the person who arrived at the answer. An LLM dumping the answer can’t elaborate on it, can’t tell the story of how they got there, etc. But it also deprives someone else of that achievement and learning. | | |
| ▲ | Ravus 2 hours ago | parent [-] | | You can see it in the way we structure college courses: engineering curricula often cover in one semester what mathematicians study over one or two years. This is because have fundamentally different goals: being able to use results in calculation versus having a deeper understanding of the subject matter. |
| |
| ▲ | KoolKat23 3 hours ago | parent | prev [-] | | You know it's valid. You're not working on incorrect assumptions. Surely there's value in that? | | |
| ▲ | datsci_est_2015 2 hours ago | parent | next [-] | | How something is proven is often more important than what is being proven. There are underlying systems and patterns that, when understood properly, improve our model of mathematical (or physical) reality. With convoluted and inelegant proofs, AI may fail to uncover those systems and patterns. As a most concrete example, it may fail to recognize some problems as isomorphic to other problems. Brute force solutions are a depth-first search. To improve human mathematical understanding, AI is probably best used as a “copilot” (lol) rather than a black box oracle, like these AI companies appear to be doing. | | |
| ▲ | KoolKat23 2 hours ago | parent [-] | | I'm sorry this framing is just moving goal posts. If you're after new methods. Then new methods is the goal, the answer to the question is not the goal then. The animated response indicates the answer wasn't just a byproduct. There is still something to glean from the answer. You have a further constraint. Otherwise whatever "new method" proposed may as well be hallucination, potentially taking you in the wrong direction away from the answer. This line of thought is not unique, stonemasons made obsolete by uniform brickword suddenly were "worried about the art and preserving traditions". |
| |
| ▲ | charlieyu1 2 hours ago | parent | prev [-] | | I don’t know if it is valid. It is unverifiable. I still found some basic algebraic mistakes in top models as late as 3-4 months ago, not sure about it now. But that’s not what I want anyway, so I often put “Do not brute force” in my prompts. | | |
| ▲ | KoolKat23 2 hours ago | parent [-] | | Sorry I mean in very public releases such as this trove, where many have lean certificates attached and publicly scrutiny. | | |
| ▲ | shakna an hour ago | parent [-] | | Three of them have already been withdrawn. So I would say we have proof, that they cannot be implicitly trusted. | | |
| ▲ | KoolKat23 an hour ago | parent [-] | | So it turns out there is a, perhaps informal, working system in place and we can deal with it. Peer reviewed and published insights are proven invalid all the time. This is the nature of research and how we learn. | | |
| ▲ | shakna an hour ago | parent [-] | | So instead of us "knowing it is valid", we don't. We need to put in extra effort, because someone felt like doing only half the work and dumping it on the community to fix. We don't know the current system can work well enough at this scale, because that's un-knowable. We know it can find some of the problems. We don't know it can find all of them. We do know it takes more effort - that's knowable. Increased data takes increased processing. Whether the community has the required effort available, seems unlikely, considering the expertise required to be able to assess these things hasn't changed. Only the ability to generate them has increased. | | |
| ▲ | KoolKat23 an hour ago | parent [-] | | You don't have to go through it. You can ignore it if you wish. There is no obligation on you to check it. I feel your concern stems from the risk that there is additional noise everyone needs to cut through. In reality this isn't any tom, dick or Harry giving you their vibe code output.
They have spent millions of dollars on this output, so there is a filter. The biggest filter of them all, funding. Furthermore, LLM's have given us another gift semantic search, we can easily check your work against theirs, this is valuable insight so instead of researchers wasting decades and fortunes pursuing an avenue that shows no value (this includes methods), they can purse new avenues they know what to avoid, in the same breath they know what to work towards. |
|
|
|
|
|
|
|
|
| ▲ | carra 4 hours ago | parent | prev | next [-] |
| > simply dumping proofs on the math community and expecting others to do the grunt work of verifying, refining, and expanding on them is hardly a productive way to advance the field. I tend to agree with this, but what is the alternative? Should OpenAI and Anthropic employ hundreds of mathematicians to do this work? Should they just not solve math problems within their reach? |
| |
| ▲ | user43928 3 hours ago | parent | next [-] | | I tend to disagree with OP, for the same reason. It's unclear what more could be expected than releasing the presumably already verified results and write-ups for each problem. Should they run a mathematics school too? Then the comment goes on to argue AI labs were not interested in actually advancing mathematics, and that investments into AI were manically excessive. IMO none of this follows and demand is there to justify the investments. The comment then goes further to argue that AI labs were putting too much effort into pretending there was exponential progress rather than actually making progress. The factual basis for this claim seems to be that OpenAI released math results and write-ups, and it's not even clear what more they could do on that topic. That's a very negative opinion. | |
| ▲ | pred_ 2 hours ago | parent | prev [-] | | Look at how actual researchers are currently using the tools: they'll generally use the LLMs to create slop papers, sometimes supported by auto-formalizations, just like OpenAI does. Then they will go through the lengthy process of digesting the results, turning the often incomprehensible and poorly organised outputs into something that humans can understand and build upon, they will then give seminars on the results, further helping with dissemination. Doing so still requires expertise, and probably will for a good while. So yes, that is exactly what they should do. Alternatively, if they are too lazy or incompetent to put in the effort themselves, do what AGMAI proposed and fund a third party to help out. |
|
|
| ▲ | alexwebb2 2 hours ago | parent | prev | next [-] |
| My steak is too juicy, my lobster is too buttery, my industry shaking mathematical proofs are coming too quickly In what world is OpenAI not “genuinely contributing to mathematics”? I’m getting whiplash from the speed at which people are suddenly accusing them, and AI in general, of not doing enough. |
| |
| ▲ | jeremyjh an hour ago | parent | next [-] | | In TFA I read (scroll up from the link anchor) this was explained: OpenAI are not giving talks - because they can't answer any questions about the model's work. There is little follow-up activity - the actual elaboration of human understanding of the new ideas is stifled since the problem is solved. But you are right, this is not OpenAI's "fault". The problem is - as others have said recently - that many people in mathematics want recognition for solving open questions more than they want the answers to the open questions. Everything about the economics and social environment of Mathematics will have to change. I think that this is exactly the same split we see in software: there are those who mainly enjoy the craft aspect of building software, and are uninterested in the product or business they are supporting. Others are primarily interested in the production of useful software or building a platform or company. I've always been in both camps myself. When it became obvious that AI was going to destroy the craft aspect - at least two years before it actually could do so - I became very discouraged, even depressed. But once it was actually good at building software, I became very excited about all the stuff I could now build. Sadly, I think a lot of people in our field have never had something they really wanted to build. | |
| ▲ | nahumfarchi an hour ago | parent | prev | next [-] | | Perhaps mathematics was never about proving things? I know it sounds like moving the goal post, and it certainly was what motivated mathematicians on a day-to-day basis, but bear with me for a moment. I think that beyond being a creative activity that humans enjoy, math was about building new tools and systems of thought. Axiomizing things we take for granted, logic, linear algebra and calculus (on which modern LLMs rely so heavily) are such examples. People chose to participate in this field because they found it enjoyable and satisfying in some way. As a side effect, society reaped the benefits every couple of centuries. Will harvesting open problems with AI ever give us these things, or will we just be left laundry pile of Lean formalizations? | |
| ▲ | gessha an hour ago | parent | prev | next [-] | | What does it mean to “genuinely” contribute to mathematics? Because the definition you use is load-bearing ;) and it might be different from that of others. | |
| ▲ | saberience an hour ago | parent | prev [-] | | Because they published a ton of slop papers with terrible English, impossible for humans (even experts) to understand, full of non-standard terms, invented jargon etc. So effectively, stuff got proved, but people don't really understand how, so it's mostly fucking useless and done for OpenAI's marketing team, while also pissing off the maths world at large. | | |
| ▲ | alexwebb2 32 minutes ago | parent [-] | | So if god himself comes down from the heavens and hands you the answers to major unsolved problems, but doesn’t walk you through them and you’ll have to still put in effort to understand them, then that’s “not contributing”? |
|
|
|
| ▲ | DesaiAshu 4 hours ago | parent | prev | next [-] |
| As with any field, convincing people to care about your ideas and your approach is half the battle Many of the best startup ideas by the best product and engineering minds failed to gain attention and funding. Same with much of the best music - relegated to hard drives with derivative ideas only resurfaced decades later I would expect much of the recent math dump will be leveraged by other LLM-driven research teams rather than read in depth by a human |
|
| ▲ | gexla 7 hours ago | parent | prev | next [-] |
| Right, easy comparison to make the the open source community for software. And it's not like this is something where we're loaned some top math genius for a limited amount of time and we have to make the most of it. Rather, this is a new high water mark. The accessibility of the results is no longer scarce. The scarcity has shifted, and that's where the focus of the math ecosystem should shift as well. And it doesn't help for a frontier community to saturate and take over messaging pipelines that were typically managed by the math ecosystem. It's not about "stay in your lane" but rather "we need coherence and be careful not to break the system." Just two cents from someone who could screw up basic cashier math on any given day. |
|
| ▲ | killerstorm 4 hours ago | parent | prev | next [-] |
| > the grunt work of verifying, refining, and expanding on them What work do you think mathematicians do normally? Like they sit whole day and have ideas? And where are the ideas? The way I see it, _some_ mathematicians enjoy solving puzzles, and now AI is better at solving puzzles. This does not affect people building new theories. Also, it's quite prestigious to write a _book_ on some topic. And guess what writing a book entails? Refining and expanding. What you call grunt work. |
| |
| ▲ | pks016 4 hours ago | parent [-] | | My grunt work is different than doing grunt work for a company to fix their problems so that they can make more money. |
|
|
| ▲ | KoolKat23 3 hours ago | parent | prev | next [-] |
| I'm sorry I disagree entirely. The more information the better. The entire purpose of published work is to remove noise (and perhaps incentivize work through attributing credit). This information is now out there. You can choose to ignore it if you wish. You may just find yourself a century behind in research. And on that point most of this research has been looked at by their mathematics panel and comes with lean certificates, it's not exactly noise. This to me is more the old guard not willing to let go or change their ways. |
| |
| ▲ | td6 3 hours ago | parent | next [-] | | I think in a ideal world your right. I think a problem is that math seems like a deeply toxic, ego driven domain. I think he argued that e.g because the navier stokes millennium problem ist considered solved now, you won't get any recognition for being the first human to solve.(How would you even proof you solved it yourself and not just regurgitated the ai proof?) And since recognition is the main objective, noone would spend time on dissecting the proof, and perhaps finding some unique approach to solving the problem, that could be transferred to other open issues. And therefore the problem is now "poisoned". Since it's assumed to be solved noone will research it, and the potential revelations won't be found | | |
| ▲ | KoolKat23 3 hours ago | parent [-] | | To be fair I'd hope during peer review this would be apparent. During your write up, I'd imagine you would check it's not already out there too. And once complete it's cheap and easy to run it through an LLM and ask is this covered by anything else out there. If its novel and not published it doesn't matter what others say. Research is already messy as it stands. Something new can already be dismissed by incumbents as "not novel enough" especially in niche fields where they're likely to be the ones conducting peer review. |
| |
| ▲ | contravariant 3 hours ago | parent | prev [-] | | I think it's quite clear the mathematics panel didn't read most of the papers with the scrutiny it would take to publish it, if only because the lean certificates and the informal proofs are not 100% the same. And if it's hard to understand (which seems to be the most common reaction) it's not exactly devoid of noise either There was an opportunity for people to work with the AI to produce a proof, now it almost feels they're working against it. | | |
| ▲ | KoolKat23 3 hours ago | parent [-] | | I never said it was journal worthy. Just its not all noise.
As I say academics are welcome to ignore it, it isn't published in any journals after all. |
|
|
|
| ▲ | willtemperley 5 hours ago | parent | prev | next [-] |
| > Too much effort is being invested in proving that the exponential curve is still holding. Given sustained exponential growth is mathematically impossible to maintain with finite resources, it's funny to me they're using advanced mathematics to try and achieve this. |
|
| ▲ | aswegs8 4 hours ago | parent | prev | next [-] |
| Once LLMs pass the threshold to being to invent new general-purpose methods and frameworks, the frontier is irreversibly lost to AI and it becomes simply a hobby that mathematicians pursue. They work through, digest, and maybe write up the proofs for understanding. But the real meat will be growing the LLMs. Who knew software eats the world was so true? |
|
| ▲ | ew-dev 3 hours ago | parent | prev | next [-] |
| > simply dumping proofs on the math community and expecting others to
> do the grunt work of verifying, refining, and expanding Hm, kinda reminds me of my college days. "Proof trivial, left as home work." was a sentence my Profs loved to say. |
|
| ▲ | schleck8 6 hours ago | parent | prev | next [-] |
| > but simply dumping proofs on the math community and expecting others to do the grunt work of verifying, refining, and expanding on them is hardly a productive way to advance the field This is a transitive period. In a few years, verification and exchange between model instances will happen faster than humans can follow. Human input will be an ethical question, and not a productivity one, because it will be the bottleneck in any science. |
| |
| ▲ | RandomLensman 3 hours ago | parent | next [-] | | How to make sure it doesn't evolve into some sort of Library of Babel of science? | | |
| ▲ | schleck8 an hour ago | parent [-] | | That's the billion dollar question. Nvidia currently wants to deploy chips with the sole purpose of monitoring agentic workloads and that doesn't seem farfetched but they obviously have a financial motive to sell more products. It's like a cat and mouse game, like cybersecurity in general. |
| |
| ▲ | Muromec 6 hours ago | parent | prev | next [-] | | And what use of that? | |
| ▲ | psychoslave 5 hours ago | parent | prev | next [-] | | Etic is a factor of productivity, and the larger the contextual window is the weightier it becomes. That’s even integrated within the paperclip parabola. If the focus in placed on maximizing some easily measurable output on a narrow perspective, situation is unlikely going to match a sweet spot of holistic equilibrium which is maximizing harmony and happiness through humanity as a whole. | |
| ▲ | nullsanity 6 hours ago | parent | prev [-] | | [dead] |
|
|
| ▲ | nateburke 2 hours ago | parent | prev | next [-] |
| Less Liszt/Paganini, more chamber music and teaching. I like it! |
|
| ▲ | FrustratedMonky an hour ago | parent | prev | next [-] |
| "community building" For what? If math is just about having a community of other mathematicians to hang out with, it still isn't a career. Nobody is paying money you need in order to to eat, just to hang out in a community. Just like a software engineer, "Well AI can write all my projects now, but I have my local Rust Users Group to hang out with". Nobody is paying me to hang out and hand code Rust. |
|
| ▲ | mastermage 6 hours ago | parent | prev | next [-] |
| Its kinda like the arms race in the cold war. There came out some truly marvelous technologies but the actualy goals were frankly terrifying. |
|
| ▲ | XorNot 7 hours ago | parent | prev | next [-] |
| That seems short sighted though. A few years ago models couldn't do this at all, I'm not sure there's any evidence to suggest exploring and refining results is outside their capabilities or will remain so. OAI obviously have a fiscal incentive here, but to presume a year from now we won't see improvements and more succinct work on the results coming from models? |
| |
| ▲ | rtpg 7 hours ago | parent | next [-] | | The problem is that one a person writes a 60 page proof in theory that person has spent an inordinate amount of time on the proof and can answer questions, describe some insight, etc etc. If a random person is given a 60 page proof to digest and not the author, those hidden insights that _aren't_ in the paper might be completely inaccessible. Maybe the AI will "just" be able to provide the insights. Maybe. But pedagogy is tricky work, and despite these AIs being able to do all this fancy math we can't get them to write good cover letters yet, so.... Ultimately we might be left with just a bunch of intellectually unsatisfying proofs. This means way less drive to simplify the proofs or rework them. End result: we generate a layer of "less efficient" mathematics, that won't get built upon. We will not actually have any shoulders upon which to stand. | | |
| ▲ | charcircuit 6 hours ago | parent | next [-] | | AI can simplify and rework proofs too. | | |
| ▲ | i_cannot_hack 6 hours ago | parent [-] | | According to Scott Aaronsson, OpenAI set their agents on 8000 different problems, and got 372 final proofs. Even spending twice the original effort on simplifying and reworking those proofs so that they do not "feel like something written by someone who’s on psychedelics" would only increase the compute by less than 10% (assuming all the agents had a similar token budget). The fact that they did not do so can only mean that either (1) their agents currently lack the capability to do it, or (2) OpenAI are completely indifferent and do not care in the slightest if the proofs are understood or not. | | |
| ▲ | gwd 5 hours ago | parent | next [-] | | > The fact that they did not do so can only mean that either (1) their agents currently lack the capability to do it, or (2) OpenAI are completely indifferent and do not care in the slightest if the proofs are understood or not. Come now, this is kind of unreasonable. When you're working on a new technology, you first get the ugly, inconvenient-to-use prototypes functioning with the core new thing you need; then you work on packaging it up into a format useable in production. I'm sure the very first digital camera sensors weren't very useful for photographers either; but it isn't really even possible to build the rest of the technology required to turn raw output of a digital sensor into something a professional photographer can use until you have the raw output itself. The research is still on going on the raw output; getting things to the next stage, where the results are widely useable by professional mathematicians (and then on to engineers and scientists to whom the results would be practically useful), is a whole new research area. | | |
| ▲ | i_cannot_hack 5 hours ago | parent [-] | | Seems like you are just subscribing to the first option I gave, "their agents currently lack the capability to do it", but saying you think they will be more capable in the future if they can move away from the inconvenient-to-use prototypes after more research. Thinking it might be possible in the future is not in disagreement with anything I said, so I am not sure what you thought was unreasonable about my description. | | |
| ▲ | gwd 2 hours ago | parent [-] | | Imagine someone looking at digital camera researchers showcasing a ground-breaking new sensor, and reacting by saying "Well obviously they're completely indifferent and do not care in the slightest if their work is used by real photographers or not." Like, "Orr... maybe they care a lot, but haven't gotten to that part yet?" | | |
| ▲ | i_cannot_hack an hour ago | parent [-] | | You are conflating the two options with each other (lack of capability vs indifference). One of them is true, not necessarily both ("or", not "and"). I did not claim a lack of capability was the same as indifference. |
|
|
| |
| ▲ | lern_too_spel 5 hours ago | parent | prev [-] | | Or (3) they feel a need to publish first, and that goal takes precedence over (2). | | |
| ▲ | i_cannot_hack 4 hours ago | parent [-] | | They claim each result used three hours of compute on average. Even spending significantly more on simplifying and reworking would delay the release with a single day at most. If avoiding such a minor delay took precedence over (2), I think "indifference" is the correct term. It has also been a while since the release now, so there is ample opportunity to post follow ups if time pressure was the only concern. | | |
| ▲ | lern_too_spel 4 hours ago | parent [-] | | Why do that when they can spend more hours extending QRH to a proof of the full Riemann Hypothesis? The opportunity cost of digging up small potatoes is the whole enchilada. |
|
|
|
| |
| ▲ | XorNot 6 hours ago | parent | prev [-] | | But why should process of discovering mathematical insights be any less attainable to AI models? The concern is being raised without evidence, because the evidence points to the gap simply being frontier models have just started to be able to get a raw proof out. Why, given existing progress, should we expect them to be unable to distill insights from those proofs? Certainly this even more likely doesn't matter at all for applications: if I can send a radio signal further because my AIs design it a certain way, that's an unambiguous result. Which is really the next step here: turn a proof into a "mechanical" application. |
| |
| ▲ | JumpCrisscross 7 hours ago | parent | prev | next [-] | | > I'm not sure there's any evidence to suggest exploring and refining results is outside their capabilities OP didn’t suggest that. The bar has been raised. Everyone has to meet it now. An inelegant solution squatted onto the internet doesn’t count as discovery per se, even if it’s impressive. | | |
| ▲ | auggierose 5 hours ago | parent [-] | | A correct solution verified in Lean will count in perpetuum. It is fine if you want more, but an achievement is an achievement, even if it is by AI. | | |
| ▲ | oliculipolicula 3 hours ago | parent [-] | | Hmmmm. It feels right that discovery is much more meaningful than achievement. "Bullshit lean proof" or "bullshit achievement" smells like it. "bullshit discovery" smells like a front-handed insult |
|
| |
| ▲ | Maxion 7 hours ago | parent | prev [-] | | But what should they do? They got all these proofs, should they just have sat on them? | | |
| ▲ | JumpCrisscross 7 hours ago | parent | next [-] | | > should they just have sat on them? It’s fine that OpenAI posted their findings. It’s not fair to claim these problems have been solved. Not until someone can understand and verify the proof and then communicate the core, novel methodological element to someone else. | | |
| ▲ | gwd 5 hours ago | parent | next [-] | | But this is Tao's point: Before, the mechanism by which a proof was verified and communicated and digested by the community was for the person who came up with the grotty, ugly first draft to engage with the community. Now there's nobody to really engage with, so the pipeline from "grotty, ugly draft" to "integrated into humanity's mathematical knowledge" has been broken. So yeah, probably we should stop saying "X has been solved", and instead say, "A Lean proof for X (or !X) has been generated". That doesn't change the fact that incentives are currently on finding the proof, and once the proof is generated by an AI, there's not currently a good mechanism / incentive structure to move that into the mathematical community. AI is here, so we need to find a new mechanism. | | |
| ▲ | lern_too_spel 5 hours ago | parent [-] | | It is not obvious to me that a single canonical human language write-up of a proof is the best output in this new world where write-ups are cheap. A human reader can query an LLM and get explanations of key points tailored to the reader's own background in mathematics. |
| |
| ▲ | CrimsonRain 5 hours ago | parent | prev | next [-] | | Solving a problem is not solving anymore. Up is down, pleasure is pain, darkness is light, slavery is freedom, madness is sanity. | |
| ▲ | Turneyboy 5 hours ago | parent | prev [-] | | Many of these are lean formalized. Arguably a much higher bar than whatever peer review provides in terms of verification. | | |
| ▲ | cmceanga 2 hours ago | parent | next [-] | | There is no guarantee that the lean proof is 1:1 with the natural language equivalent. The lean proof can be lesser. This happened in the Navier-Stokes proof, e.g. see [1] in example 3.1. Having the certificate doesn't necessarily imply correctness. [1] https://arxiv.org/abs/2610.08144 | |
| ▲ | psychoslave 5 hours ago | parent | prev [-] | | On some consideration, surely. On the other hand, but at some point this is borderline like saying "universe already solved every physical problems, including possibility to represent deep important point of its own structure in compressed intelligent ways" and then tell that reaching it in an actual grabbable artifact is left as an exercise. Possibly yes such a representation is possible. But it doesn’t mean it’s certain there is a "best compressed representation". And even less one that encompass everything important and that is understandable by any human brain, even the most exceptionally brilliant ones sponsored by a whole society to reach their best possible achievable performance on that goal through full dedication on that sole task. |
|
| |
| ▲ | usernomdeguerre 7 hours ago | parent | prev | next [-] | | >They got all these proofs... Your phrasing is illuminating that perhaps they aren't engaged in the creation, understanding, or integration of these proofs by humanity; they just have them. For them, this is a slidedeck they can pass to investors, creditors, the marketing department. Something they can add to the employee onboarding pamphlet. What should they do? Hyperbolic maybe, but perhaps engage with humanity. | | | |
| ▲ | p_hoep 7 hours ago | parent | prev | next [-] | | No need. In the end the mathematicians that don't like this can just not look at the proofs or use them. They have that choice. Just like they didn't "ask" for them, they don't have to even acknowledge they exist. | |
| ▲ | sans_souse 6 hours ago | parent | prev | next [-] | | BlackBox: The proof is in the pudding This isn't only bad for Math — it's bad for English too. 'Proof' is going to become the 2026 Most Misapplied Word of the Year. | |
| ▲ | pks016 4 hours ago | parent | prev | next [-] | | At least check them properly. They have already withdrawn some of them. | |
| ▲ | 6 hours ago | parent | prev [-] | | [deleted] |
|
|
|
| ▲ | myzek 5 hours ago | parent | prev | next [-] |
| Generate and dump on others to verify is how the generative-AI people operate. Be it in maths or just your regular job. The amount of Confluence pages of "research" that is just a dump of LLM output someone passed to me to review is staggering I hate this approach, it's unbelievably selfish |
|
| ▲ | yieldcrv 4 hours ago | parent | prev | next [-] |
| > There seems to be more interest in hitting some arbitrary benchmark (we proved X unsolved problems) than in genuinely contributing to mathematics I feel the same way about academia, the papers, the citations, the ego, the narcissism and the taxpayer codependency that got cut off and turns out wasn’t necessary at all thanks to a private sector entity running laps around them I don’t feel that academics need to pursue the discipline and distributed brain-wracking that has sometimes resulted in the solved math problems, just because more times they find other nooks and crannies to explore along the way. I think the blueprint is enough. Standing on the shoulders of giants is good enough. and if the concern is that they can’t figure out what to do with a proof, next year’s AI will |
|
| ▲ | mrheosuper 7 hours ago | parent | prev | next [-] |
| Why not asking another chatbot to verify, like what we are doing with coding ? |
| |
| ▲ | kadoban 7 hours ago | parent | next [-] | | That's not the hard part. The hard part still requires humans (and/or _maybe_ a bunch of tokens) and a lot of work. | |
| ▲ | iterance 6 hours ago | parent | prev [-] | | And then what? |
|
|
| ▲ | caaqil 6 hours ago | parent | prev | next [-] |
| > There seems to be more interest in hitting some arbitrary benchmark (we proved X unsolved problems) > genuinely contributing to mathematics What's the difference between the two? Proofs are no longer the goalpost? |
| |
| ▲ | tene80i 6 hours ago | parent | next [-] | | Proofs are valuable but I believe the mathematical community values understanding more. Proofs were previously a great way to develop understanding. Now, less so. | |
| ▲ | shubhamjain 6 hours ago | parent | prev | next [-] | | Not an expert, but explaining the proof and it being independently verifiable as important as just putting a paper of it. Reminds me of 1000 page proof of Goldbach’s conjecture that a Mathematician reached sometime back. He was told plainly that no one is going to invest time in verifying the proof because there’s a good chance there’s an error somewhere in between. | |
| ▲ | desterothx 5 hours ago | parent | prev | next [-] | | Proofs of open problems are valuable because we are assuming that proving the problem requires some new method or infrastructure in math to prove it. Basically proving open problems isn't actually useful if it doesn't develop new tooling for mathematics, which can help us create new open problems, solve other ones etc. | |
| ▲ | pegasus 5 hours ago | parent | prev [-] | | I recommend RTFA, it explains exactly that: why proofs should not be considered the goalpost, and why dumping all these AI-generated proofs might be an overall negative for mathematics as a whole. |
|
|
| ▲ | flexie 7 hours ago | parent | prev | next [-] |
| Yes, it is indeed a balanced view. Those few thousand mathematicians are now getting a taste of their own medicine. After all, it was people with extraordinary mathematical talent who developed machine learning and large language models, leaving hundreds of millions of people who earn their living through speaking, writing, or teaching worried about their future job prospects. Still, I believe almost everyone will be fine. Perhaps AI will also prove good at coming up with new conjectures, and some mathematicians may shift towards applied mathematics or other sciences. |
| |
| ▲ | FrustratedMonky an hour ago | parent [-] | | Pretty tenuous connection to blame mathematicians for everything bad created in the world, that happened to use math. |
|
|
| ▲ | encyclopediai 5 hours ago | parent | prev [-] |
| This Math 1.0 followed by Math 2.0 framing is wrong. Mathematics did not start a few decades ago when problem solving became the norm. And it will not end now when problem solving turns out to be "easy". Mathematics will revert to it's main practice, which is to study. There are lots of weird panic reactions by some prominent problem solvers. See for example the ridiculous cease and desist like statement of AHM shared at Tao blog. Put this Math 1-2.0 with that AHM statement together and you'll realize that this is a power struggle and that you see only one side of it. Mathematicians have very diverse opinions about this. I, for example, am for as much as possible automatic harvesting of all these "low hanging" fruits. Should be disclosed as soon as possible, free of any bottleneck, and citable. The mathematics community may do whatever its various members desire to do with these results. Let them decide individually what to do with them. This AI tool is here to stay. |
| |
| ▲ | encyclopediai 4 hours ago | parent [-] | | This looks indeed like a public relations campaign, it would be helpful to the conversation to contribute your opinion, in a polite way. |
|