I'm a mathematics student, so this is near to my heart and I'd like to weigh in with an insider's perspective and try to write a faux FAQ (with the caveat that I'm still early in my studies, so...
Exemplary
I'm a mathematics student, so this is near to my heart and I'd like to weigh in with an insider's perspective and try to write a faux FAQ (with the caveat that I'm still early in my studies, so anyone here with more knowledge is welcome to offer corrections/disagreement.)
How important are these problems?
There are ~400 of them so it varies quite a bit. However, the most important ones are, basically, very important. A lot have been outstanding for decades, and are pretty central in their various subfields. The Millennium problems have developed a bit of a mythology around them, so the recent Navier-Stokes solution got a lot of attention, but I (subjectively) think this batch of problems is probably more of an achievement.
Are the solutions correct?
Again because of how many there are, it's not possible to say definitively yet. I will say that my personal opinion is that probably most of them are correct. For people who aren't in the know, a big project in math/CS has been formal proof verification. Simply put, this is a way to write math proofs in a way that computers can check their correctness. Because of the propensity of LLMs to spew out giant chunks devoid of meaning, a focus has been specifically on training LLMs to write proofs in Lean (a programming language for computer-checkable proofs), to reduce the amount of slop necessary to wade through. The complication here is that these Lean proofs themselves need to be verified, i.e., a 'proof' might assert True while actually proving something subtly different from the natural-language question. So to reiterate, although the existence of a Lean proof is a strong sign for correctness, it still needs oversight. But OpenAI does employ mathematicians, and it would be very embarrassing if more than a handful of solutions were flawed, so I think when the dust settles, we'll find most are correct.
Did they steal the solutions from the work of mathematicians in their training data?
Probably not. I know this idea got a lot of traction due to the circumstances around the Navier-Stokes solution, and I think that particular case is more up-in-the-air. Here, the quantity and complexity of the problems make it much less plausible. Moreover, mathematics as a discipline checks most/all of the boxes for a domain which an LLM can excel in, so I think we've unfortunately just reached that point.
You said 'unfortunately', but isn't this a good thing? Isn't this a rare example of AI unambiguously helping further human knowledge?
That depends on who you ask. If you ask a mathematician, the answer will rather be unambiguously 'no'. Or, maybe that's being a bit dramatic and it's more complicated? My personal take, which I glean is shared by most mathematicians, is along these lines:
OpenAI has no interest in doing right by the mathematical community, and is using this mainly as a publicity stunt.
Now that the solutions exist, it's good they're public, but this isn't how most mathematicians wanted the solutions to be found.
It's extremely worrying that the means to advance an entire domain of knowledge are proprietary and not publicly available.
In a worst case scenario, this could kill mathematics as a discipline.
And I think it's especially easy to write off mathematician's concerns here along the lines of "Yes, this is really tragic for mathematicians, but for progress/knowledge in general, this seems like a net good". For some perspective, (this may seem like a truism) the way mathematicians think about math is very different from the way other people think about math. There was a very good post shared here some months ago titled "The Fall of the Theorem Economy" which I recommend reading, the general thesis of which goes like this: In the eyes of the public, mathematicians solve mathematical problems, and this is what determines their worth as a mathematician. In the eyes of mathematicians, mathematicians study/invent/communicate knowledge of mathematical objects, and among the surest ways to understand these objects is through the posing/answering of problems about them, where these problems also serve as a practical benchmark for assessing mathematical skill.
Just like every other knowledge field, we're confronting the situation where 'domain knowledge' is no longer all that necessary for the production of competent domain work. It's selfish of me to say, but I really think this is especially terrible for the field of mathematics. The reason is, most fields have something to latch onto, but in mathematics, the work is the field in many ways. Mathematical questions are sufficiently abstract that they are meaningful basically only insofar as you understand the content of the question. The threat posed by AI of removing the need for understanding is, in the case of mathematics, the threat of removing the ability to engage with mathematics at all. It is a bit like automating philosophy, and hence why mathematicians are losing their shit and not entirely able to articulate why to a general audience.
...the process of exploring a problem has frequently led to new conceptual models and new discoveries; prioritising solutions over process can trivially cut short those incentives and risk losing...
...the process of exploring a problem has frequently led to new conceptual models and new discoveries; prioritising solutions over process can trivially cut short those incentives and risk losing that engine of innovation...
I have a layperson (maybe dumb) question... Where do the mathematical problems that are being solved here come from? Or I guess another way to put that is, how do we become aware of these problems...
I have a layperson (maybe dumb) question... Where do the mathematical problems that are being solved here come from? Or I guess another way to put that is, how do we become aware of these problems that need solving in the first place? And once they are solved, do they typically have some practical application that can benefit from that solution?
The mathematical problems usually also come from mathematicians, and this often happens in a recursive way. Basically, Mathematician A might be trying to solve an existing problem, and maybe they...
The mathematical problems usually also come from mathematicians, and this often happens in a recursive way. Basically, Mathematician A might be trying to solve an existing problem, and maybe they come to the realization that the problem is just a specific example of a more general idea. Then Mathematician A tries to nail down exactly what that more general idea is, which they do by trying to come up with a satisfactory definition that encapsulates the properties of the idea in a nice way.
Once they have a new definition of a new idea, the immediate next question is "What are the properties of this definition, and how does it relate to existing definitions?" Maybe by thinking deeply about the idea, they become convinced that the definition implies some other property, but they're not sure how to prove it. They might publish their work so far, along with some of the main conjectures/hypotheses they came up with, at which point Mathematician B picks up the torch, and the cycle repeats.
The practical applications basically vary on a case-by-case basis, and can even change over time (number theory was totally useless until it found applications in cryptography) Some math problems are purely for the love of the game-- they're genuinely useless and serve no purpose other than to advance math.
Other problems do have some direct application. For example, in this batch of OpenAI problems, they claimed to have shown a new lower bound on the computational complexity of complex matrix multiplication. Basically, matrices are rectangles of entries (think an Excel spreadsheet), and they can be multiplied together in a funny way that doesn't really match what the common idea of multiplication means. The important part is huge amounts of computer technologies rely on matrix multiplication, and in fact LLMs themselves do. With that in mind, it's very desirable to try to find the most computationally efficient way to multiply matrices together, and one of the OpenAI proofs claims to have shown that the most efficient way (for a specific kind of matrix) is more efficient than was previously believed.
Editing to add on: What Asinine said is also worth noting, where if you follow the chain of problems back far enough, there's usually a question about a real-life problem at the root.
As a mostly layperson (who took enough classes in other studies for a two-year math degree and managed to tack on a minor in math for a four-year), I believe most are just theories. Some are...
As a mostly layperson (who took enough classes in other studies for a two-year math degree and managed to tack on a minor in math for a four-year), I believe most are just theories. Some are rooted in a [mostly-]tangible concept, like the Theory of Relativity, the heat equation, or quantum gravity. Some spin off from those or other ideas, but I believe most are derived from trying to explain or solve real-life things --though some are pulled way out of their original line of study for creation of other equations that may explain something else. That last bit I feel is where most fall, though I really was a layperson stumbling through the field. I followed most of evergoe's post above (which, btw, is great different perspective than what I had, thank you for something new to chew on!), but I still feel I likely resonate more with the general population.
Until we as human beings realise that most often the best “interest” is for the greater good and that it actually pays off both financially and beneficially in the end these solutions can’t really...
• OpenAI has no interest in doing right by the mathematical community, and is using this mainly as a publicity stunt.
Until we as human beings realise that most often the best “interest” is for the greater good and that it actually pays off both financially and beneficially in the end these solutions can’t really be trusted as a whole. Just my idealistic reasoning I know.
• Now that the solutions exist, it's good they're public, but this isn't how most mathematicians wanted the solutions to be found.
This is difficult for a layman as me to understand because it makes it sound like a survival cry for a whole occupation (which is totally understandable) but still feels weird. If the solution is there why not use it and maybe work backwards. Is it because we don’t understand how we got there and in it loses our control and checks and balances of math?
As you probably can tell I know next to nothing about math and I’m sorry if you’ve already addressed this previously. Thank you for a very insightful comment.
In its most idealized form, math develops in a very organic way, where mathematicians gain a deeper understanding of the ideas introduced by the previous generation, manage to solve many of the...
In its most idealized form, math develops in a very organic way, where mathematicians gain a deeper understanding of the ideas introduced by the previous generation, manage to solve many of the problems posed by that generation, and then introduce their own set of ideas and problems.
Although math is generally portrayed as an objective field, mathematical definitions really are more of a creative/artistic endeavor. They might be introduced because they 'seem' like the aesthetically 'right' way to think about an idea, and gain widespread acceptance for the same reason, and even be modified over time as we become more aware of the nuances of an idea.
AI sort of threatens to sever this thread, by destroying this organic development. It's a bit like it's offering a 'Next Episode' button, but after pressing it over and over, we're in Season 7 and not really sure what's going on.
You're right that we can try to work backwards from the solutions, but that's easier said than done. Setting aside how deeply soulless playing janitor for an LLM would be, it's really not for lack of trying that these problems/ideas can take decades or centuries to come to fruition. They really can be subtle enough that it requires the sensibilities of the entire mathematical community to develop over time until the circumstances permit progress. It's something like historical consciousness, where it just doesn't seem possible to fast-track it, even with a later stage as an exemplar.
Obviously the above concern is predicated on the ideas that (a) It's intellectually/spiritually worthwhile to understand math, and (b) Humans will remain necessary in some form for mathematical progress. If we let go of those ideas, then all bets are off, but at this point in time that seems reckless.
Do you think there's something to the idea that a major issue with being handed AI solutions is that we miss out on a lot of valuable understanding and insight in the process of working through...
Do you think there's something to the idea that a major issue with being handed AI solutions is that we miss out on a lot of valuable understanding and insight in the process of working through the problems (the real math was the friends we made along the way). I've heard that argument before, and I would love to believe it, but it doesn't sit right with me. It seems like that value is only there for the ones who actually solve the thing and everyone else who comes along after is standing on the shoulders of those giants regardless of if it's Ai or human solved. Maybe I'm misunderstanding the process though.
My background is in physics (though I also have a degree in math), so take my opinion as you will. Pure mathematics, as I understand it, is done for the love of the game. This is also true for...
My background is in physics (though I also have a degree in math), so take my opinion as you will.
Pure mathematics, as I understand it, is done for the love of the game. This is also true for academia in general, but non-mathematicians tend to underestimate just how abstract mathematics can be, how disconnected it is from application. Most research mathematics is going to be totally inscrutable to anyone who isn't a mathematician. So the issue isn't that AI is unfair to mathematicians by being better at proving results; it's more like: if mathematicians are the only ones who are equipped to appreciate the work, and you cut out the mathematicians, then who is the actual audience for these results (especially since AI proofs are usually inscrutable to mathematicians, too)?
Just as an example, here is a recent abstract from the arXiv, chosen at random. Good luck finding a practical application.
Surface braids are a generalization of braids to surfaces in the 4-disk. They are described by planar graphs called charts, and sequences of braid words called braid systems, that represent monodromies of branch points in projections. Yang-Baxter operators (YBOs) have been used extensively in knot theory for constructions of Jones and other polynomials, defined by braid group representations. We propose to use YBOs for constructing surface braid invariants through braid systems. The intersections of eigenspaces are used for this construction. We further use 3-cocycles of the Yang-Baxter cohomology theories via charts, in an analogue of quandle cocycle invariants but more generally utilizing tensor products of modules. An approach towards defining knotted surface invariants through closures of surface braids is discussed.
Okay, so you might ask: if mathematics is only done for other mathematicians, then doesn't that make mathematics a parasitic, self-indulgent pleasure? Well, no. If mathematics is the wilderness, and the applied sciences are the tourist stops, then mathematicians are the navigators who guide us between the sights. If you were to replace all human mathematicians with agent mathematicians, we humans would be lost in the wilds forever. There would never be that chance for a mathematician to encounter a biologist at a dinner party and comment that, "Ah, your particular [protein folding problem] reminds me of [obscure mathematical theory]." Who else but the mathematician is willing to get a little lost in the weeds?
Much like reading, for high-level math, the value is in the journey of understanding, not just the ending. The main point isn't developing proofs, it's furthering the understanding of math....
Much like reading, for high-level math, the value is in the journey of understanding, not just the ending. The main point isn't developing proofs, it's furthering the understanding of math. Spitting out proofs is part of that, but if the proof that is spit out is unintelligible to humans, it defeats the purpose.
Of course, now that public scrutiny is opening up they're finding they have to redact and amend them, and based on what's happening there, it looks like a lot of these are citing each other, so redacting one will have cascading effects for the validity of many of them.
From the article: To me it just smells like they found another instance where there's enough training data out there that they can steal, and the models can be hyper-focused on, to produce results...
From the article:
“There’s likely to be a bunch of results where they take someone’s work and then take it to completion,” Dr. Buckmaster said in an interview on Monday evening.
With so many results released at once, “I don’t think they’ve done their sort of due diligence at all,” he said.
To me it just smells like they found another instance where there's enough training data out there that they can steal, and the models can be hyper-focused on, to produce results that sound impressive and will get them impressive sounding headlines. So now of course they're driving a truck through it to drum up as much hype as possible. I (like, I assume, most people) don't know enough about how solving these math problems works to know how impressive this actually is, which is probably why OpenAI is going so hard on it right now.
Also huge dumps like this make good headlines, and harder for people to independently verify before the headline drops off the news cycle. And there's that "responsibly release the model" line,...
Also huge dumps like this make good headlines, and harder for people to independently verify before the headline drops off the news cycle.
And there's that "responsibly release the model" line, which I'm convinced is industry code for "we would go bankrupt if we released this because there is no way we could get people to pay the price required to do this profitably."
Related, how's that IPO going Sam? Gonna push it again?
I'd bet also that a model that's been hyper-tuned to write mathematics proofs is probably not very good at anything else, so it wouldn't be useful as a general purpose model that everyday users...
I'd bet also that a model that's been hyper-tuned to write mathematics proofs is probably not very good at anything else, so it wouldn't be useful as a general purpose model that everyday users would see any benefit from (and might even be embarrassing for them once people started prodding at it).
This math is beyond any of us. They are problems we’ve never heard of before and we’re trusting mathematicians to tell us their significance. The results haven’t been verified but mathematicians...
This math is beyond any of us. They are problems we’ve never heard of before and we’re trusting mathematicians to tell us their significance. The results haven’t been verified but mathematicians are taking them seriously.
So this “oh they’re stealing it” just seems like cope. It’s time to admit that AI is better at grinding out theorems than people are. Certainly better than all of us, probably better than nearly all mathematicians, and if it’s not quite better than every mathematician, it’s just a matter of time. Compare with what happened with chess and Go.
I don't disagree that computers in general may already or one day be better than human mathematicians at solving certain types of problems. I disagree that LLMs are the most likely path to get us...
I don't disagree that computers in general may already or one day be better than human mathematicians at solving certain types of problems. I disagree that LLMs are the most likely path to get us there though. You accuse my skepticism of being cope, but to state things like LLMs are "better than nearly all mathematicians" based on the info we have right now seems absolutely bonkers to me, so I think we're just operating on completely different wavelengths when it comes to LLMs.
I have no independent information. It's based on what actual mathematicians are saying. They are worried and expect that if mathematics survives, it will be entirely different. Is AI the End of...
I have no independent information. It's based on what actual mathematicians are saying. They are worried and expect that if mathematics survives, it will be entirely different.
“In whatever years I have left, I don’t expect that I’ll ever again prove a theorem because I’m actually needed to prove it,” Scott Aaronson of the University of Texas, Austin wrote on his blog. “Human mathematicians are forevermore dethroned as the main theorem-proving entities on planet earth.” Other online missives expressed optimism, but many revealed some combination of grief, confusion, and fear.
...
Two days after the announcement, I found myself in a classroom at the University of California, Berkeley, surrounded by some 150 students, postdocs, and professors. The mathematician Ken Ono, who took a leave of absence from the University of Virginia to work at an AI start-up called Axiom Math, was scheduled to give a talk. “You might be graduating into a profession that might not even exist, or that will be very different than what you expected,” Ono told them. “You need to brace.”
The audience responded with anger and frustration. There were whispers and exchanged glances; Ono couldn’t make it through a single slide without a fresh wave of questions. “I’m not entirely sure what our takeaway is supposed to be,” one student said. Another asked how Ono and his start-up would take responsibility in light of “the shameful way that AI companies are treating mathematics.”
Software engineers are saying similar things about programming, and I'm not convinced of that either. There's too much hype, too much fresh fear and uncertainty, and too many corporate interests...
Software engineers are saying similar things about programming, and I'm not convinced of that either. There's too much hype, too much fresh fear and uncertainty, and too many corporate interests in pushing these kinds of extreme narratives for me to take any of it without a massive grain of salt and rolling my eyes a bit.
I think there's value in the comparison to coding: People have been saying software engineering as a profession will be dead by next tuesday for a number of years now. So far they've been...
I think there's value in the comparison to coding:
People have been saying software engineering as a profession will be dead by next tuesday for a number of years now. So far they've been profoundly wrong about that. The profession is changing rather than dying. A future leap could change the course but wild speculation has proven to be the opposite of useful up to this point.
The people making the wild speculations generally fall onto a handful of camps: People who have something to gain from the hype, people who know next to nothing about software engineering, and software engineers who don't yet have a reasonable understanding of the technology and its limitations. Also a subset of the latter camp: software engineers who are terrified and reacting emotionally without sufficient information.
I think we're seeing something similar in mathematics. The people who are saying that mathematics as a profession is dead are just making wild claims. Mathematics as a profession is changing. We don't know what that change will look like yet and we should take the opinions of even professional mathematicians with a grain of salt unless they've had extensive experience with agent assisted math, deeply understand the strengths and limitations, and have had time to get past the heady, overexcited, period following the initial mind blown moment and had time to come back down to earth. Those are the people who will be able to offer useful insights into how things might evolve.
IMO those are also the people who would ideally be pushing the frontier forward, as opposed to anonymous OAI employees running an unreleased proprietary model for the sole purpose of generating hype that can be parlayed into future funding rounds.
I would argue that while "programming" or "software engineering" may still exist, "coding" basically is over as a thing that humans do. There are still exceptions, it will take time for the impact...
I would argue that while "programming" or "software engineering" may still exist, "coding" basically is over as a thing that humans do. There are still exceptions, it will take time for the impact of coding assistants to be felt evenly, etc., but having humans bang out code simply isn't economical anymore for basically any purpose.
"Software engineering" may still exist because we still need to produce software; and, furthermore, that does still want domain expertise. Someone with prior experience as a programmer is, at least for now, going to be better at getting their LLM to do the right thing. But for high-level math, the practical utility is unclear; and when it does have practical utility, it's usually not in merely knowing whether a given theorem is true or false.
I disagree that coding is going away. I think we still don't know what that future looks like, and LLMs will certainly play a part (especially if they ever become economically viable in a way that...
I disagree that coding is going away. I think we still don't know what that future looks like, and LLMs will certainly play a part (especially if they ever become economically viable in a way that doesn't 100% rely on the worst, greediest billionaires in the world and destroying our planet), but I believe there will always be value in prioritizing a tight code base, and building and maintaining institutional knowledge over how that code actually works, and the more you rely on LLMs to do all your coding for you the more those things necessarily get sacrificed. Nobody gets into software engineering because they like reading code, and that will go a hundred fold when we're talking about reading LLM generated code. There's a reason that "vibe coding" is so derided--it produces shit. A world where "'coding' is basically over" is a world where everything is essentially vibe coded garbage and I very strongly disagree that will ever take over the industry as a whole.
I quite like reading code and using an LLM as a power tool to clean up the codebase whenever I see code I don’t like. I’m writing a web app to help at reading and searching TypeScript, much like...
I quite like reading code and using an LLM as a power tool to clean up the codebase whenever I see code I don’t like. I’m writing a web app to help at reading and searching TypeScript, much like an IDE, but read-only. I’ve largely stopped using a text editor. I’ll probably add editing for Markdown files, though, because LLMs are still terrible at writing documentation.
I think you're already wrong. What we knew as coding is already going away. Almost no one I know at work still uses an IDE or text editor, at least very rarely. The problem with hand coding...
I think you're already wrong. What we knew as coding is already going away.
Almost no one I know at work still uses an IDE or text editor, at least very rarely. The problem with hand coding outside of a hobby or profession is that AI can get something 95% correct in a fraction of the time. And that correct percentage is on an upwards march.
Most of the people I know and work with do still use IDEs (even the ones who have adopted LLMs into their projects and workflow). I'm not really saying that developers who rely on LLMs to generate...
Most of the people I know and work with do still use IDEs (even the ones who have adopted LLMs into their projects and workflow). I'm not really saying that developers who rely on LLMs to generate all their code don't or won't exist, I'm just saying that developers who don't do that aren't going away any time soon and which type of developer you aspire to be (one who writes code, or one who writes no code and instead reviews and iterates on LLM generated code) will be a choice, and that both of those choices will remain a valid one, each with its own pros and cons and attractiveness to developers with different values and skillsets.
So far, in my personal experience where I work, that does not seem to be the way things are going. It's entirely possible that I'm biased. I work on software for the aerospace industry (primarily...
Exemplary
So far, in my personal experience where I work, that does not seem to be the way things are going.
It's entirely possible that I'm biased. I work on software for the aerospace industry (primarily NASA), and our software is used and relied on in a way such that bugs in certain portions of the code could literally cost human lives. When a mission critical bug is found, it's extremely stressful even when you're working together with engineers who know the codebase intricately because they were involved in every step of its development—architecture, logic design and decisions, down to writing the code by hand themselves. I can't even imagine how much more stressful it would be if nobody actually knew the code, or only understood it as vague high-level abstractions, and instead of a bunch of experts scrutinizing the code that they all wrote together to find and fix the problem, you'd have to read and trust a bunch of sycophantic word salad LLM output about it. That idea is absolutely terrifying and I can't imagine a world where we'd all just be fine with it.
OK, yes I would say you are biased :P Fair enough I agree that anyone writing aerospace code or MISRA C anywhere is going to have other factors requiring more reliability than AIs can currently...
OK, yes I would say you are biased :P
Fair enough I agree that anyone writing aerospace code or MISRA C anywhere is going to have other factors requiring more reliability than AIs can currently deliver. That is not true for most software, and I don't think it's something that will necessarily stay true forever, it's possible in the future we can get much higher performance and reliability from AIs than from engineers even at system scales.
And I think the problem is that the decisionmakers are becoming increasingly abstracted from knowing whether their coders should be in that reliability camp or not. My car's infotainment screen...
And I think the problem is that the decisionmakers are becoming increasingly abstracted from knowing whether their coders should be in that reliability camp or not.
My car's infotainment screen should be in that reliability camp. It quite obviously is not. It is very distressing.
A timely comment in light of Margaret Hamilton’s passing. I can’t imagine astronauts entrusting their lives to vibe-coded control systems. That day may come, and sooner than we like. Hopefully not...
A timely comment in light of Margaret Hamilton’s passing. I can’t imagine astronauts entrusting their lives to vibe-coded control systems.
That day may come, and sooner than we like. Hopefully not with actual dire consequences.
I've created a data migration pipeline using primarily LLMs, and it's frankly quite terrifying that anybody might use this process for any code that is meant to exist for more than a few months.
I've created a data migration pipeline using primarily LLMs, and it's frankly quite terrifying that anybody might use this process for any code that is meant to exist for more than a few months.
The next frontier there is going to be software both produced and verified by AI. It's probably not worth the time and money for frontier labs to train that capability right now, but there's no...
The next frontier there is going to be software both produced and verified by AI. It's probably not worth the time and money for frontier labs to train that capability right now, but there's no reason why they can't get there eventually.
See, I think this just isn't thinking far enough ahead. Give it a few more years, and you don't need humans to have institutional knowledge about how the code works.
institutional knowledge over how that code actually works
See, I think this just isn't thinking far enough ahead. Give it a few more years, and you don't need humans to have institutional knowledge about how the code works.
Without refuting the fact that it's likely there is now a piece of software that may outclass humans at working out theorems, they still fucking suck at outputting something that isn't filled with...
Without refuting the fact that it's likely there is now a piece of software that may outclass humans at working out theorems, they still fucking suck at outputting something that isn't filled with falsehoods. Just today I had to repeatedly reign in my AI because it couldn't stop confusing itself when the conversation went on. Not uncommon in any field that uses AI.
I'm sure that, at least for the foreseeable future, human mathematicians will be required to prove that the output of the machine is indeed proof or if it again acted like a pokemon hit with supersonic halfway through the match.
Eventually we may see a system whose output we can take at face value. That's when I will worry about the human cost (more than I do now).
Pretty much all of the math work LLMs do make use of formal proof engines. (So does human work, fyi, it's just a useful tool to make sure you're being rigorous) Using a proof engine doesn't mean...
Pretty much all of the math work LLMs do make use of formal proof engines.
(So does human work, fyi, it's just a useful tool to make sure you're being rigorous)
Using a proof engine doesn't mean that a human doesn't have to verify the output, but it means that the surface area of what you have to check is small. You need to check the axioms the LLM was assuming, but from there it all must proceed in a logical and correct manner.
So
or if it again acted like a pokemon hit with supersonic halfway through the match.
is not a problem. Their work is constrained by logical formalisms. The middle will be correct as long as the beginning is.
Oh, I agree that when it comes to programming, it will often do crazy things if given half a chance. But I think there some problems where you have to try AI, because it only has to be right once,...
Oh, I agree that when it comes to programming, it will often do crazy things if given half a chance.
But I think there some problems where you have to try AI, because it only has to be right once, and what if it finds something? For example, scanning for security bugs. If you don't scan for security bugs and fix them, someone else will use AI to find the bugs instead.
And it seems like proving mathematical theorems might be an "it only has to be right once" kind of problem? The failed attempts get thrown out. If there's decent chance of success, it can just keep trying until it gets it.
And like with other tools you might use, a human often has to interpret the results.
You are. I don't know if you've noticed or not, but @skybrian is something an AI booster. That user is the source of many if not most of the AI hype-cycle links posted here these days. They reply...
I think we're just operating on completely different wavelengths when it comes to LLMs.
You are. I don't know if you've noticed or not, but @skybrian is something an AI booster. That user is the source of many if not most of the AI hype-cycle links posted here these days. They reply in strong terms whenever anyone criticizes the claims made by OpenAI et al., to the point that I would say they occasionally dip a toe over the line of Tildes's number one rule. But as skybrian is an established power user here, and as Deimos appears pretty disinterested in doing much with Tildes any longer, I wouldn't expect anything much to happen because of it.
I suggest not engaging with them on this topic. I don't think they're interested in the same kind of discussion about it that you or many others of us are.
That feels like a pretty unfair reading of said user. I think skybrian is a believer in AI, but that’s not a crime nor against the rules of the site. I have never seen them reply in a way that...
That feels like a pretty unfair reading of said user. I think skybrian is a believer in AI, but that’s not a crime nor against the rules of the site. I have never seen them reply in a way that remotely dips over the line.
“AI booster” seems to imply that they’re like a plant or something, which I see no reason to be true. A person can believe in the capability of AI just because that’s what they believe.
I think "booster" vs "believer" is a distinction without a difference. I have, to the point that I'm not particularly concerned with being charitable about it. I will be civil about it though,...
I think "booster" vs "believer" is a distinction without a difference.
I have never seen them reply in a way that remotely dips over the line.
I have, to the point that I'm not particularly concerned with being charitable about it. I will be civil about it though, which is why I phrased my response as I did. I've seen a few instances in which Skybrian's demeanor while discussing this subject flirts with disrespect for their interlocutors, but I've always refrained from commenting before now.
Skybrian is more than welcome to their opinion, which is why I suggested not engaging with them if you are an AI skeptic. There's just no point to it.
Honestly, I don't find your comments here civil at all. You engaged in name-calling. You suggest that this user or his comments should be removed from the site, and the only reason they aren't is...
I will be civil about it
Honestly, I don't find your comments here civil at all. You engaged in name-calling. You suggest that this user or his comments should be removed from the site, and the only reason they aren't is lack of moderation. You advise others to ignore this user. I was a hair away from labeling your comment malice, but I decided to comment instead.
I feel like you did have a good piece of advice here, but I'd like to reflect it back a bit. I don't see how your comments here are contributing to the discussion. You're right that one does not need to engage in discussions they're not interested in. If you've come here just to badmouth a frequent contributor to the site, I'd say that you are in fact violating Tildes' number one rule.
I hope you will take this as feedback rather than fighting.
There's a pretty big difference in connotation. If someone went up to you and said, "look at that guy, he's a racial equality booster", you'd probably think that the guy who went up to you is...
I think "booster" vs "believer" is a distinction without a difference.
There's a pretty big difference in connotation.
If someone went up to you and said, "look at that guy, he's a racial equality booster", you'd probably think that the guy who went up to you is racist, because booster is used almost entirely negatively.
I've seen with a few instances in which Skybrian's demeanor while discussing this subject flirts with disrespect for their interlocutors
You should report those posts, then. Deimos isn't updating the site, but that doesn't mean he doesn't read the reports. He usually even DMs you if he doesn't choose to act.
Skybrian is more than welcome to their opinion, which is why I suggested not engaging with them if you are an AI skeptic.
I mean, you can do whatever you want, it's your life and it's just a online forum, but intellectually it's more beneficial to challenge your beliefs against people who hold the opposite rather than people with the same beliefs. That doesn't mean you need to "win" the conversation, but it's nonetheless a useful exercise in having a more rounded view of the world. So that's the point - it's not to like "win" against skybrian, it's just to challenge your own beliefs.
In this thread, for instance, while skybrian is just a dude, their point is true that many incredibly intelligent and accomplished mathematicians have the belief that LLMs are strong in their ability to work on mathematical theorems. Terrance Tao, the GOAT, for instance. That's worth stewing on IMO.
I don't think it's cope. If the solution for the math problem incorporated components of research as training data and then solved the math problem without citing the research, it feels...
I don't think it's cope. If the solution for the math problem incorporated components of research as training data and then solved the math problem without citing the research, it feels intellectually dishonest. The model didn't solve this, the corpus of human research did.
The findings are great, but the way they released them may not be. If they don’t cite sources, collaborate, or follow a real process they are potentially damaging the ability for mathematicians to...
The findings are great, but the way they released them may not be. If they don’t cite sources, collaborate, or follow a real process they are potentially damaging the ability for mathematicians to generate new credible research for them to train on in the future.
This is a messy process, but it seems more likely that having power tools will increase the productivity of mathematicians rather than decrease it, compared to doing everything by hand. The...
This is a messy process, but it seems more likely that having power tools will increase the productivity of mathematicians rather than decrease it, compared to doing everything by hand.
The remaining work that's not automated becomes more important. For example, apparently the math papers generated by these tools are pretty badly written. Verification is partially automated, but still needs to be done.
In many fields, scientists use tools to do the actual experiments, but the scientists still need to plan the experiments and write up the results. It looks like math will become more like an experimental science. Mathematicians will depend on AI like astronomers depend on telescopes.
Mathematicians don't have these tools. OpenAI does. They own them, and control them. The tools aren't open source, open weight, or otherwise public/free. They can use them sure, but this isn't the...
Mathematicians don't have these tools. OpenAI does. They own them, and control them. The tools aren't open source, open weight, or otherwise public/free.
They can use them sure, but this isn't the same as handing a mathematician a computer, open source software, or a calculator. It's a service. To run a local model that gets near these flagship models you are probably spending $10,000+ on local hardware, even then it's probably not the same.
These tools also require, currently, humans to create novel concepts and supply it with information to train on.
Is there a potential feature where LLMs hollow out the entry level of so many professions that the data we generate for future LLMs to train on can stagnate?
Scientists also don't own submarines, space telescopes or particle accelerators, but it's still possible to fund expensive scientific instruments and negotiate access. Big science is still science.
Scientists also don't own submarines, space telescopes or particle accelerators, but it's still possible to fund expensive scientific instruments and negotiate access. Big science is still science.
All I'm saying is that OpenAI could've released these findings following the normal process mathematicians use to do so. They could've cited inspirations and sources and worked with the community...
All I'm saying is that OpenAI could've released these findings following the normal process mathematicians use to do so. They could've cited inspirations and sources and worked with the community instead of just dumping the results as a big public relations and marketing scheme. They aren't doing this to advance human knowledge, they are doing this to make their company look more valuable to investors.
Apparently the most important result is a proof of the "Unique Games Conjecture." Here's a 2011 article about it. To me it sounds like a good name for a band, but what do I know?
Apparently the most important result is a proof of the "Unique Games Conjecture." Here's a 2011 article about it.
To me it sounds like a good name for a band, but what do I know?
I love a good band name taken from a relatively obscure reference. My top pick in that category is The Airborne Toxic Event from the Novel (and subsequent movie) White Noise, which I greatly...
I love a good band name taken from a relatively obscure reference. My top pick in that category is The Airborne Toxic Event from the Novel (and subsequent movie) White Noise, which I greatly enjoyed and fully recommend to anyone that enjoys absurdism.
On Tuesday, OpenAI deluged mathematicians with hundreds of new findings that span a wide swath of topics including algebra, number theory, theoretical computer science, mathematical logic and topology.
The 377 results follow OpenAI’s announcement last month that it had succeeded in cracking the Navier-Stokes equation — one of the so-called Millennium Problems, which were considered so challenging that a $1 million reward was offered for each solution.
[...]
Like the Navier-Stokes result, the new mathematical solutions used a more advanced A.I. model that has not been released publicly.
I haven't read them all but this one had a new perspective for me.
JOHANNES SCHMITT
One thing to keep in mind about this drop of papers is that they were not created by OpenAI with the main goal of making progress in mathematical research, or even primarily for PR (there were some PR posts, but e.g. the final announcement was comparatively restrained). The main reason these papers exist is that OpenAI used unsolved math problems to evaluate their internal models for the purpose of improving their capabilities. They had to use hard open problems because these are the only ones still posing a challenge to frontier AI models. I believe that, from OpenAI’s point of view, the papers are essentially a byproduct of their internal development.
Thus the company could just have remained silent, or picked a few flashy results for another blog post. I think it is to their credit that instead they reached out to the math community for guidance on how to proceed, leading to the formation of the Advisory Group on Mathematics and Artificial Intelligence. They followed some of the advice by this group, such as a timely release and (partial) Lean certificates, but not all of it, and in particular announced that they will continue to use open math problems for model development. In my view, the most pressing need of the math community right now is to have a central platform to discuss the results, start digesting the (by multiple accounts from colleagues, terribly written) papers, and report any mathematical mistakes or missing attribution. An OpenAI-controlled GitHub repository, with issues and pull requests disabled, cannot serve this purpose, and the ball is in OpenAI’s court to move the papers to a neutral repository and to back such a community effort with the promised funding for workshops and special programs.
I had not considered how these math problems are natural benchmarks for evaluating model capabilities. They are unsolved, yet verifiable, and also "cheap" to attempt since you don't have to set up physical environments, run clinical trials, etc.
EDIT: There are many thoughtful and emotive reactions in the blog post. Worth reading
I'm a mathematics student, so this is near to my heart and I'd like to weigh in with an insider's perspective and try to write a faux FAQ (with the caveat that I'm still early in my studies, so anyone here with more knowledge is welcome to offer corrections/disagreement.)
How important are these problems?
There are ~400 of them so it varies quite a bit. However, the most important ones are, basically, very important. A lot have been outstanding for decades, and are pretty central in their various subfields. The Millennium problems have developed a bit of a mythology around them, so the recent Navier-Stokes solution got a lot of attention, but I (subjectively) think this batch of problems is probably more of an achievement.
Are the solutions correct?
Again because of how many there are, it's not possible to say definitively yet. I will say that my personal opinion is that probably most of them are correct. For people who aren't in the know, a big project in math/CS has been formal proof verification. Simply put, this is a way to write math proofs in a way that computers can check their correctness. Because of the propensity of LLMs to spew out giant chunks devoid of meaning, a focus has been specifically on training LLMs to write proofs in Lean (a programming language for computer-checkable proofs), to reduce the amount of slop necessary to wade through. The complication here is that these Lean proofs themselves need to be verified, i.e., a 'proof' might assert True while actually proving something subtly different from the natural-language question. So to reiterate, although the existence of a Lean proof is a strong sign for correctness, it still needs oversight. But OpenAI does employ mathematicians, and it would be very embarrassing if more than a handful of solutions were flawed, so I think when the dust settles, we'll find most are correct.
Did they steal the solutions from the work of mathematicians in their training data?
Probably not. I know this idea got a lot of traction due to the circumstances around the Navier-Stokes solution, and I think that particular case is more up-in-the-air. Here, the quantity and complexity of the problems make it much less plausible. Moreover, mathematics as a discipline checks most/all of the boxes for a domain which an LLM can excel in, so I think we've unfortunately just reached that point.
You said 'unfortunately', but isn't this a good thing? Isn't this a rare example of AI unambiguously helping further human knowledge?
That depends on who you ask. If you ask a mathematician, the answer will rather be unambiguously 'no'. Or, maybe that's being a bit dramatic and it's more complicated? My personal take, which I glean is shared by most mathematicians, is along these lines:
And I think it's especially easy to write off mathematician's concerns here along the lines of "Yes, this is really tragic for mathematicians, but for progress/knowledge in general, this seems like a net good". For some perspective, (this may seem like a truism) the way mathematicians think about math is very different from the way other people think about math. There was a very good post shared here some months ago titled "The Fall of the Theorem Economy" which I recommend reading, the general thesis of which goes like this: In the eyes of the public, mathematicians solve mathematical problems, and this is what determines their worth as a mathematician. In the eyes of mathematicians, mathematicians study/invent/communicate knowledge of mathematical objects, and among the surest ways to understand these objects is through the posing/answering of problems about them, where these problems also serve as a practical benchmark for assessing mathematical skill.
Just like every other knowledge field, we're confronting the situation where 'domain knowledge' is no longer all that necessary for the production of competent domain work. It's selfish of me to say, but I really think this is especially terrible for the field of mathematics. The reason is, most fields have something to latch onto, but in mathematics, the work is the field in many ways. Mathematical questions are sufficiently abstract that they are meaningful basically only insofar as you understand the content of the question. The threat posed by AI of removing the need for understanding is, in the case of mathematics, the threat of removing the ability to engage with mathematics at all. It is a bit like automating philosophy, and hence why mathematicians are losing their shit and not entirely able to articulate why to a general audience.
...the process of exploring a problem has frequently led to new conceptual models and new discoveries; prioritising solutions over process can trivially cut short those incentives and risk losing that engine of innovation...
I have a layperson (maybe dumb) question... Where do the mathematical problems that are being solved here come from? Or I guess another way to put that is, how do we become aware of these problems that need solving in the first place? And once they are solved, do they typically have some practical application that can benefit from that solution?
The mathematical problems usually also come from mathematicians, and this often happens in a recursive way. Basically, Mathematician A might be trying to solve an existing problem, and maybe they come to the realization that the problem is just a specific example of a more general idea. Then Mathematician A tries to nail down exactly what that more general idea is, which they do by trying to come up with a satisfactory definition that encapsulates the properties of the idea in a nice way.
Once they have a new definition of a new idea, the immediate next question is "What are the properties of this definition, and how does it relate to existing definitions?" Maybe by thinking deeply about the idea, they become convinced that the definition implies some other property, but they're not sure how to prove it. They might publish their work so far, along with some of the main conjectures/hypotheses they came up with, at which point Mathematician B picks up the torch, and the cycle repeats.
The practical applications basically vary on a case-by-case basis, and can even change over time (number theory was totally useless until it found applications in cryptography) Some math problems are purely for the love of the game-- they're genuinely useless and serve no purpose other than to advance math.
Other problems do have some direct application. For example, in this batch of OpenAI problems, they claimed to have shown a new lower bound on the computational complexity of complex matrix multiplication. Basically, matrices are rectangles of entries (think an Excel spreadsheet), and they can be multiplied together in a funny way that doesn't really match what the common idea of multiplication means. The important part is huge amounts of computer technologies rely on matrix multiplication, and in fact LLMs themselves do. With that in mind, it's very desirable to try to find the most computationally efficient way to multiply matrices together, and one of the OpenAI proofs claims to have shown that the most efficient way (for a specific kind of matrix) is more efficient than was previously believed.
Editing to add on: What Asinine said is also worth noting, where if you follow the chain of problems back far enough, there's usually a question about a real-life problem at the root.
As a mostly layperson (who took enough classes in other studies for a two-year math degree and managed to tack on a minor in math for a four-year), I believe most are just theories. Some are rooted in a [mostly-]tangible concept, like the Theory of Relativity, the heat equation, or quantum gravity. Some spin off from those or other ideas, but I believe most are derived from trying to explain or solve real-life things --though some are pulled way out of their original line of study for creation of other equations that may explain something else. That last bit I feel is where most fall, though I really was a layperson stumbling through the field. I followed most of evergoe's post above (which, btw, is great different perspective than what I had, thank you for something new to chew on!), but I still feel I likely resonate more with the general population.
Until we as human beings realise that most often the best “interest” is for the greater good and that it actually pays off both financially and beneficially in the end these solutions can’t really be trusted as a whole. Just my idealistic reasoning I know.
This is difficult for a layman as me to understand because it makes it sound like a survival cry for a whole occupation (which is totally understandable) but still feels weird. If the solution is there why not use it and maybe work backwards. Is it because we don’t understand how we got there and in it loses our control and checks and balances of math?
As you probably can tell I know next to nothing about math and I’m sorry if you’ve already addressed this previously. Thank you for a very insightful comment.
In its most idealized form, math develops in a very organic way, where mathematicians gain a deeper understanding of the ideas introduced by the previous generation, manage to solve many of the problems posed by that generation, and then introduce their own set of ideas and problems.
Although math is generally portrayed as an objective field, mathematical definitions really are more of a creative/artistic endeavor. They might be introduced because they 'seem' like the aesthetically 'right' way to think about an idea, and gain widespread acceptance for the same reason, and even be modified over time as we become more aware of the nuances of an idea.
AI sort of threatens to sever this thread, by destroying this organic development. It's a bit like it's offering a 'Next Episode' button, but after pressing it over and over, we're in Season 7 and not really sure what's going on.
You're right that we can try to work backwards from the solutions, but that's easier said than done. Setting aside how deeply soulless playing janitor for an LLM would be, it's really not for lack of trying that these problems/ideas can take decades or centuries to come to fruition. They really can be subtle enough that it requires the sensibilities of the entire mathematical community to develop over time until the circumstances permit progress. It's something like historical consciousness, where it just doesn't seem possible to fast-track it, even with a later stage as an exemplar.
Obviously the above concern is predicated on the ideas that (a) It's intellectually/spiritually worthwhile to understand math, and (b) Humans will remain necessary in some form for mathematical progress. If we let go of those ideas, then all bets are off, but at this point in time that seems reckless.
Do you think there's something to the idea that a major issue with being handed AI solutions is that we miss out on a lot of valuable understanding and insight in the process of working through the problems (the real math was the friends we made along the way). I've heard that argument before, and I would love to believe it, but it doesn't sit right with me. It seems like that value is only there for the ones who actually solve the thing and everyone else who comes along after is standing on the shoulders of those giants regardless of if it's Ai or human solved. Maybe I'm misunderstanding the process though.
My background is in physics (though I also have a degree in math), so take my opinion as you will.
Pure mathematics, as I understand it, is done for the love of the game. This is also true for academia in general, but non-mathematicians tend to underestimate just how abstract mathematics can be, how disconnected it is from application. Most research mathematics is going to be totally inscrutable to anyone who isn't a mathematician. So the issue isn't that AI is unfair to mathematicians by being better at proving results; it's more like: if mathematicians are the only ones who are equipped to appreciate the work, and you cut out the mathematicians, then who is the actual audience for these results (especially since AI proofs are usually inscrutable to mathematicians, too)?
Just as an example, here is a recent abstract from the arXiv, chosen at random. Good luck finding a practical application.
Okay, so you might ask: if mathematics is only done for other mathematicians, then doesn't that make mathematics a parasitic, self-indulgent pleasure? Well, no. If mathematics is the wilderness, and the applied sciences are the tourist stops, then mathematicians are the navigators who guide us between the sights. If you were to replace all human mathematicians with agent mathematicians, we humans would be lost in the wilds forever. There would never be that chance for a mathematician to encounter a biologist at a dinner party and comment that, "Ah, your particular [protein folding problem] reminds me of [obscure mathematical theory]." Who else but the mathematician is willing to get a little lost in the weeds?
Much like reading, for high-level math, the value is in the journey of understanding, not just the ending. The main point isn't developing proofs, it's furthering the understanding of math. Spitting out proofs is part of that, but if the proof that is spit out is unintelligible to humans, it defeats the purpose.
Of course, now that public scrutiny is opening up they're finding they have to redact and amend them, and based on what's happening there, it looks like a lot of these are citing each other, so redacting one will have cascading effects for the validity of many of them.
From the article:
To me it just smells like they found another instance where there's enough training data out there that they can steal, and the models can be hyper-focused on, to produce results that sound impressive and will get them impressive sounding headlines. So now of course they're driving a truck through it to drum up as much hype as possible. I (like, I assume, most people) don't know enough about how solving these math problems works to know how impressive this actually is, which is probably why OpenAI is going so hard on it right now.
Also huge dumps like this make good headlines, and harder for people to independently verify before the headline drops off the news cycle.
And there's that "responsibly release the model" line, which I'm convinced is industry code for "we would go bankrupt if we released this because there is no way we could get people to pay the price required to do this profitably."
Related, how's that IPO going Sam? Gonna push it again?
I'd bet also that a model that's been hyper-tuned to write mathematics proofs is probably not very good at anything else, so it wouldn't be useful as a general purpose model that everyday users would see any benefit from (and might even be embarrassing for them once people started prodding at it).
This math is beyond any of us. They are problems we’ve never heard of before and we’re trusting mathematicians to tell us their significance. The results haven’t been verified but mathematicians are taking them seriously.
So this “oh they’re stealing it” just seems like cope. It’s time to admit that AI is better at grinding out theorems than people are. Certainly better than all of us, probably better than nearly all mathematicians, and if it’s not quite better than every mathematician, it’s just a matter of time. Compare with what happened with chess and Go.
I don't disagree that computers in general may already or one day be better than human mathematicians at solving certain types of problems. I disagree that LLMs are the most likely path to get us there though. You accuse my skepticism of being cope, but to state things like LLMs are "better than nearly all mathematicians" based on the info we have right now seems absolutely bonkers to me, so I think we're just operating on completely different wavelengths when it comes to LLMs.
I have no independent information. It's based on what actual mathematicians are saying. They are worried and expect that if mathematics survives, it will be entirely different.
Is AI the End of Math As We Know It?
...
Software engineers are saying similar things about programming, and I'm not convinced of that either. There's too much hype, too much fresh fear and uncertainty, and too many corporate interests in pushing these kinds of extreme narratives for me to take any of it without a massive grain of salt and rolling my eyes a bit.
I think there's value in the comparison to coding:
I think we're seeing something similar in mathematics. The people who are saying that mathematics as a profession is dead are just making wild claims. Mathematics as a profession is changing. We don't know what that change will look like yet and we should take the opinions of even professional mathematicians with a grain of salt unless they've had extensive experience with agent assisted math, deeply understand the strengths and limitations, and have had time to get past the heady, overexcited, period following the initial mind blown moment and had time to come back down to earth. Those are the people who will be able to offer useful insights into how things might evolve.
IMO those are also the people who would ideally be pushing the frontier forward, as opposed to anonymous OAI employees running an unreleased proprietary model for the sole purpose of generating hype that can be parlayed into future funding rounds.
I would argue that while "programming" or "software engineering" may still exist, "coding" basically is over as a thing that humans do. There are still exceptions, it will take time for the impact of coding assistants to be felt evenly, etc., but having humans bang out code simply isn't economical anymore for basically any purpose.
"Software engineering" may still exist because we still need to produce software; and, furthermore, that does still want domain expertise. Someone with prior experience as a programmer is, at least for now, going to be better at getting their LLM to do the right thing. But for high-level math, the practical utility is unclear; and when it does have practical utility, it's usually not in merely knowing whether a given theorem is true or false.
I disagree that coding is going away. I think we still don't know what that future looks like, and LLMs will certainly play a part (especially if they ever become economically viable in a way that doesn't 100% rely on the worst, greediest billionaires in the world and destroying our planet), but I believe there will always be value in prioritizing a tight code base, and building and maintaining institutional knowledge over how that code actually works, and the more you rely on LLMs to do all your coding for you the more those things necessarily get sacrificed. Nobody gets into software engineering because they like reading code, and that will go a hundred fold when we're talking about reading LLM generated code. There's a reason that "vibe coding" is so derided--it produces shit. A world where "'coding' is basically over" is a world where everything is essentially vibe coded garbage and I very strongly disagree that will ever take over the industry as a whole.
I quite like reading code and using an LLM as a power tool to clean up the codebase whenever I see code I don’t like. I’m writing a web app to help at reading and searching TypeScript, much like an IDE, but read-only. I’ve largely stopped using a text editor. I’ll probably add editing for Markdown files, though, because LLMs are still terrible at writing documentation.
I think you're already wrong. What we knew as coding is already going away.
Almost no one I know at work still uses an IDE or text editor, at least very rarely. The problem with hand coding outside of a hobby or profession is that AI can get something 95% correct in a fraction of the time. And that correct percentage is on an upwards march.
Most of the people I know and work with do still use IDEs (even the ones who have adopted LLMs into their projects and workflow). I'm not really saying that developers who rely on LLMs to generate all their code don't or won't exist, I'm just saying that developers who don't do that aren't going away any time soon and which type of developer you aspire to be (one who writes code, or one who writes no code and instead reviews and iterates on LLM generated code) will be a choice, and that both of those choices will remain a valid one, each with its own pros and cons and attractiveness to developers with different values and skillsets.
I don't think they will go away, lots of people enjoy programming. I think it will become economically unfeasible to employ them.
So far, in my personal experience where I work, that does not seem to be the way things are going.
It's entirely possible that I'm biased. I work on software for the aerospace industry (primarily NASA), and our software is used and relied on in a way such that bugs in certain portions of the code could literally cost human lives. When a mission critical bug is found, it's extremely stressful even when you're working together with engineers who know the codebase intricately because they were involved in every step of its development—architecture, logic design and decisions, down to writing the code by hand themselves. I can't even imagine how much more stressful it would be if nobody actually knew the code, or only understood it as vague high-level abstractions, and instead of a bunch of experts scrutinizing the code that they all wrote together to find and fix the problem, you'd have to read and trust a bunch of sycophantic word salad LLM output about it. That idea is absolutely terrifying and I can't imagine a world where we'd all just be fine with it.
OK, yes I would say you are biased :P
Fair enough I agree that anyone writing aerospace code or MISRA C anywhere is going to have other factors requiring more reliability than AIs can currently deliver. That is not true for most software, and I don't think it's something that will necessarily stay true forever, it's possible in the future we can get much higher performance and reliability from AIs than from engineers even at system scales.
And I think the problem is that the decisionmakers are becoming increasingly abstracted from knowing whether their coders should be in that reliability camp or not.
My car's infotainment screen should be in that reliability camp. It quite obviously is not. It is very distressing.
A timely comment in light of Margaret Hamilton’s passing. I can’t imagine astronauts entrusting their lives to vibe-coded control systems.
That day may come, and sooner than we like. Hopefully not with actual dire consequences.
I've created a data migration pipeline using primarily LLMs, and it's frankly quite terrifying that anybody might use this process for any code that is meant to exist for more than a few months.
The next frontier there is going to be software both produced and verified by AI. It's probably not worth the time and money for frontier labs to train that capability right now, but there's no reason why they can't get there eventually.
See, I think this just isn't thinking far enough ahead. Give it a few more years, and you don't need humans to have institutional knowledge about how the code works.
We'll just have to agree to disagree on that one, to me that is an absolutely insane take.
Without refuting the fact that it's likely there is now a piece of software that may outclass humans at working out theorems, they still fucking suck at outputting something that isn't filled with falsehoods. Just today I had to repeatedly reign in my AI because it couldn't stop confusing itself when the conversation went on. Not uncommon in any field that uses AI.
I'm sure that, at least for the foreseeable future, human mathematicians will be required to prove that the output of the machine is indeed proof or if it again acted like a pokemon hit with supersonic halfway through the match.
Eventually we may see a system whose output we can take at face value. That's when I will worry about the human cost (more than I do now).
Pretty much all of the math work LLMs do make use of formal proof engines.
(So does human work, fyi, it's just a useful tool to make sure you're being rigorous)
Using a proof engine doesn't mean that a human doesn't have to verify the output, but it means that the surface area of what you have to check is small. You need to check the axioms the LLM was assuming, but from there it all must proceed in a logical and correct manner.
So
is not a problem. Their work is constrained by logical formalisms. The middle will be correct as long as the beginning is.
Oh, I agree that when it comes to programming, it will often do crazy things if given half a chance.
But I think there some problems where you have to try AI, because it only has to be right once, and what if it finds something? For example, scanning for security bugs. If you don't scan for security bugs and fix them, someone else will use AI to find the bugs instead.
And it seems like proving mathematical theorems might be an "it only has to be right once" kind of problem? The failed attempts get thrown out. If there's decent chance of success, it can just keep trying until it gets it.
And like with other tools you might use, a human often has to interpret the results.
You are. I don't know if you've noticed or not, but @skybrian is something an AI booster. That user is the source of many if not most of the AI hype-cycle links posted here these days. They reply in strong terms whenever anyone criticizes the claims made by OpenAI et al., to the point that I would say they occasionally dip a toe over the line of Tildes's number one rule. But as skybrian is an established power user here, and as Deimos appears pretty disinterested in doing much with Tildes any longer, I wouldn't expect anything much to happen because of it.
I suggest not engaging with them on this topic. I don't think they're interested in the same kind of discussion about it that you or many others of us are.
That feels like a pretty unfair reading of said user. I think skybrian is a believer in AI, but that’s not a crime nor against the rules of the site. I have never seen them reply in a way that remotely dips over the line.
“AI booster” seems to imply that they’re like a plant or something, which I see no reason to be true. A person can believe in the capability of AI just because that’s what they believe.
It’s OK for people have differing beliefs.
I think "booster" vs "believer" is a distinction without a difference.
I have, to the point that I'm not particularly concerned with being charitable about it. I will be civil about it though, which is why I phrased my response as I did. I've seen a few instances in which Skybrian's demeanor while discussing this subject flirts with disrespect for their interlocutors, but I've always refrained from commenting before now.
Skybrian is more than welcome to their opinion, which is why I suggested not engaging with them if you are an AI skeptic. There's just no point to it.
Honestly, I don't find your comments here civil at all. You engaged in name-calling. You suggest that this user or his comments should be removed from the site, and the only reason they aren't is lack of moderation. You advise others to ignore this user. I was a hair away from labeling your comment malice, but I decided to comment instead.
I feel like you did have a good piece of advice here, but I'd like to reflect it back a bit. I don't see how your comments here are contributing to the discussion. You're right that one does not need to engage in discussions they're not interested in. If you've come here just to badmouth a frequent contributor to the site, I'd say that you are in fact violating Tildes' number one rule.
I hope you will take this as feedback rather than fighting.
There's a pretty big difference in connotation.
If someone went up to you and said, "look at that guy, he's a racial equality booster", you'd probably think that the guy who went up to you is racist, because booster is used almost entirely negatively.
You should report those posts, then. Deimos isn't updating the site, but that doesn't mean he doesn't read the reports. He usually even DMs you if he doesn't choose to act.
I mean, you can do whatever you want, it's your life and it's just a online forum, but intellectually it's more beneficial to challenge your beliefs against people who hold the opposite rather than people with the same beliefs. That doesn't mean you need to "win" the conversation, but it's nonetheless a useful exercise in having a more rounded view of the world. So that's the point - it's not to like "win" against skybrian, it's just to challenge your own beliefs.
In this thread, for instance, while skybrian is just a dude, their point is true that many incredibly intelligent and accomplished mathematicians have the belief that LLMs are strong in their ability to work on mathematical theorems. Terrance Tao, the GOAT, for instance. That's worth stewing on IMO.
I don't think it's cope. If the solution for the math problem incorporated components of research as training data and then solved the math problem without citing the research, it feels intellectually dishonest. The model didn't solve this, the corpus of human research did.
And yet, the effect on mathematicians is the same however it did it.
The findings are great, but the way they released them may not be. If they don’t cite sources, collaborate, or follow a real process they are potentially damaging the ability for mathematicians to generate new credible research for them to train on in the future.
This is a messy process, but it seems more likely that having power tools will increase the productivity of mathematicians rather than decrease it, compared to doing everything by hand.
The remaining work that's not automated becomes more important. For example, apparently the math papers generated by these tools are pretty badly written. Verification is partially automated, but still needs to be done.
In many fields, scientists use tools to do the actual experiments, but the scientists still need to plan the experiments and write up the results. It looks like math will become more like an experimental science. Mathematicians will depend on AI like astronomers depend on telescopes.
Mathematicians don't have these tools. OpenAI does. They own them, and control them. The tools aren't open source, open weight, or otherwise public/free.
They can use them sure, but this isn't the same as handing a mathematician a computer, open source software, or a calculator. It's a service. To run a local model that gets near these flagship models you are probably spending $10,000+ on local hardware, even then it's probably not the same.
These tools also require, currently, humans to create novel concepts and supply it with information to train on.
Is there a potential feature where LLMs hollow out the entry level of so many professions that the data we generate for future LLMs to train on can stagnate?
Scientists also don't own submarines, space telescopes or particle accelerators, but it's still possible to fund expensive scientific instruments and negotiate access. Big science is still science.
All I'm saying is that OpenAI could've released these findings following the normal process mathematicians use to do so. They could've cited inspirations and sources and worked with the community instead of just dumping the results as a big public relations and marketing scheme. They aren't doing this to advance human knowledge, they are doing this to make their company look more valuable to investors.
I don't think it's a coincidence that this is only a week after it came out that they're seeking another $30b of funding.
Definitely not the same. Local models are great but they don’t scale by just throwing more compute at them.
Apparently the most important result is a proof of the "Unique Games Conjecture." Here's a 2011 article about it.
To me it sounds like a good name for a band, but what do I know?
I love a good band name taken from a relatively obscure reference. My top pick in that category is The Airborne Toxic Event from the Novel (and subsequent movie) White Noise, which I greatly enjoyed and fully recommend to anyone that enjoys absurdism.
From the article:
[...]
There's a math blog hosting mathematician reactions to this announcement. Figured some of you might want to see more commentary too. https://proofsandprompts.com/2026/10/08/100-reactions-to-100-solutions/
I haven't read them all but this one had a new perspective for me.
I had not considered how these math problems are natural benchmarks for evaluating model capabilities. They are unsolved, yet verifiable, and also "cheap" to attempt since you don't have to set up physical environments, run clinical trials, etc.
EDIT: There are many thoughtful and emotive reactions in the blog post. Worth reading