Last night my 9-year-old son was taunting my wife, complexity theorist Dana Moshkovitz, as follows: “mommy, I heard you got cooked! I heard that a robot solved the math problem you worked on for your whole career! OOF!”
While my son was being a brat, he also wasn’t wrong. Whether you’re thrilled, depressed, angry, or whatever else about it, yesterday was surely one of the biggest days in mathematical history. And yes, among the 372 huge results released yesterday by OpenAI, on the recommendation of its advisory group of Timothy Gowers, Edward Witten, and other distinguished mathematicians, was a proof of Subhash Khot’s Unique Games Conjecture (UGC), a statement that my wife has worked toward proving for the entire time I’ve known her. (The UGC implies that a whole slew of optimization problems really are NP-hard, even if you just want an approximation that’s slightly better than what you get from semidefinite programming relaxation, which is one of our main tools.)
Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet; the race to do so has just started. If you want an on-the-ground sense of what that race is going to be like, here’s some of what Dana texted me last night:
It feels like something written by someone who’s on psychedelics. So much unclear and doesn’t make sense. Lots of name dropping of previous work without discussing why it can be used despite impossibility results
Basically the paper is so horribly written that it’s impossible to read it without AI help
I asked Astra for reasonable completeness and soundness claims of the noise gadget and it gave them by combining claims from all over the paper
[...]
The citations are often irrelevant and confusing
A possible future is a math world that’s heavenly if you have vision/creative ideas that AI could help check and implement.
And of course there’s a lot for us to learn from the aliens
If you’re wondering what emotions Dana is feeling—well, probably all of them! Even while a central career aspiration has fallen to a robot, there are at least two mitigating factors for her. First, she can feel vindicated that the UGC was true after all, something she never doubted even while many of her colleagues did! Second, all of us in math and theoretical computer science and mathematical physics, at least those who cared about solving crisply-stated problems, are now in the same boat.
[...]
These have emerged as the two main models for communicating AI math breakthroughs, and they both have strengths and weaknesses. The “OpenAI model” sets up a crazy race among humans to digest and explain a messy AI proof (work that could easily be some combination of thankless, barely-credited, competitive, and unfun), while the “Anthropic model” puts a private company in the position of picking and choosing which human mathematicians get to be the emissaries of the AI. Dunno, what do you guys think?
For those who are wondering: apparently, the AI model that produced all these wonders was not bespoke contraption of 10,000 agents burning millions of dollars worth of compute, as was used for example to construct a finite-time blowup for the Navier-Stokes equations. Instead, it was simply the latest internal OpenAI model—one that might be released to paying ChatGPT customers within the next couple of months, depending on the recommendations of OpenAI’s safety board! (My 9-year-old son: “Oh they definitely shouldn’t release that. If it could solve all those math problems, it can’t possibly be safe.”) Apparently they used about 3 hours of GPT-Pro level compute on average per problem solved.
Also, if you were wondering: apparently they tried the model on about 8,000 problems. So, right now it “merely” solves ~5% of the longstanding open mathematical problems that it’s asked about, the problems that whole communities have spent years on, after a single 3-hour attempt on them.
[...]
If you want some sense of what things feel like now in math, imagine a hunter-gatherer who’s spent his entire life learning to survive deep in an unforgiving rainforest, then a giant resort hotel springs up right next to him with a helipad and heated pools and AirBnBs, and without missing a beat, the hunter-gatherer says: “alright fine, so now my new job is to run wilderness retreats for the tourists, or something.”
This is honestly a pretty good way of putting it, in my opinion. One of the very last courses I took before graduating with a math degree just this year was a philosophy of math course. We were...
If you want some sense of what things feel like now in math, imagine a hunter-gatherer who’s spent his entire life learning to survive deep in an unforgiving rainforest, then a giant resort hotel springs up right next to him with a helipad and heated pools and AirBnBs, and without missing a beat, the hunter-gatherer says: “alright fine, so now my new job is to run wilderness retreats for the tourists, or something.”
This is honestly a pretty good way of putting it, in my opinion. One of the very last courses I took before graduating with a math degree just this year was a philosophy of math course. We were discussing what the impacts of AI on the mathematical profession would be more-or-less right when AI started getting good at math. I think the general consensus then was that the actual grinding out of proofs would fall to the machine, but the actual asking of questions and posing of conjectures (and understanding what we actually learned from conjectures being true or false!) was still solidly in the human realm.
Suffice to say, a very interesting time indeed right now!
This is quite something. I keep having the thought repeatedly: Another one (profession) bites the dust. Programmers, digital artists, animators, various analysts - business, economics, law..., now...
This is quite something. I keep having the thought repeatedly: Another one (profession) bites the dust. Programmers, digital artists, animators, various analysts - business, economics, law..., now theoretical mathematicians.
And no, don't lie to yourself that AI is not and will never be good in any of this - we are long past the phase when it was good enough in many fields, now we are in the one when it is the best (and cheap) approach to many of them - as we see here.
Who will put food on our tables?
The writing is absolutely on the wall and news stories like the one I heard on the radio this morning "this just in AI is NOT taking our jobs" based on some report that it's slowing show how much...
The writing is absolutely on the wall and news stories like the one I heard on the radio this morning "this just in AI is NOT taking our jobs" based on some report that it's slowing show how much we love plunging our heads in the sand.
Whatever the pace, our gerentocracy political class are demonstrating once again that they're not able to keep pace with the impact of changing times.
It's weird cause like, if your job is JUST pushing out code, then yea, AI is going to take your job. But the reality is many programmers write code for like 1/3rd of their time, and communicate...
It's weird cause like, if your job is JUST pushing out code, then yea, AI is going to take your job. But the reality is many programmers write code for like 1/3rd of their time, and communicate across teams, managers, etc the other 2/3 of the time. Sure, AI replaces the code bit such that things that used to take weeks now take me hours to do, which means I could write more code but... the rest of the workflow still hasn't caught up, testing is still slow by nature unless we wanna give up and just have bugs in production like Github does. Planning is still slow, people still take a month to talk about shit before they make a ticket, etc.
Most of my day is spent sitting around and talking about "Do we even really want to do this feature?" or "Is this thing a customer reported actually a bug?" and maybe AI could do that if we told it to, but stakeholders don't want to talk to AI, they want to talk to the developer team. The architect leading the project is going to ask me about the code that I let the AI write and you better believe I'm expected to understand it. The companies that are letting AI just do everything have already found out the hard way that it leads to shitty software, looking at you, Github.
So, I think, while right now it seems like we need less developers, I think it'll end up like the cotton gin - there will be this really expensive task that's a part of the workflow that AI can't do, and we'll hire "developers" who are really just "code managers" who can do that task of being the Subject Matter Expert of the code they let the AI write.
And you don't think AI will be able to handle that eventually? It's currently being given the ability to do all the basic tasks. But what happens when it learns how to manage projects (semi- and...
And you don't think AI will be able to handle that eventually? It's currently being given the ability to do all the basic tasks. But what happens when it learns how to manage projects (semi- and then fully) autonomously? Nearly every time I hear someone describe reasons AI isn't taking any jobs, it seems to be reasons current AI isn't currently taking (m)any jobs.
Yeah I mean, maybe? But the thing is that people like being in charge. They like managing their own projects. They like talking to other people who manage other projects. Like, fast food...
Yeah I mean, maybe? But the thing is that people like being in charge. They like managing their own projects. They like talking to other people who manage other projects.
Like, fast food restaurants still have counters and drive thrus even though we’ve had the technology to replace those things for at least 20 years and it’s been commonly used for about the last 10 years. Most people prefer the self checkout, but the human option still exists for those who need custom service for accessibility reasons or whatever else.
It’ll end up like, if AI can manage projects, you’ll just have 1 project manager managing like 50 projects at once instead of ~5 that they can do now. We’ll still have the same number of everyone, but they’ll produce way more way faster.
I am sorry if I am making a stupid question. This is not my field and maybe I am naive... But if no one understands the proof how can we know it is valid?
I am sorry if I am making a stupid question. This is not my field and maybe I am naive... But if no one understands the proof how can we know it is valid?
I think @evergoe comment in the other thread helped explain this. Basically the proofs are written in a machine-checkable form and they passes the logic test. Human still need to check if those...
I think @evergoecomment in the other thread helped explain this. Basically the proofs are written in a machine-checkable form and they passes the logic test. Human still need to check if those versions are actually congruent to the original problems but at least one barrier has cleared.
To get a better sense of how messy the situation is, see also this preprint: "Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural...
To get a better sense of how messy the situation is, see also this preprint:
In particular, this preprint alleges that while the result for Navier-Stokes appears to be correct (i.e. the lean proof does in fact prove the right claim), OpenAI's paper does not match the lean proof. So in this case, we do not actually know whether the paper proof is correct, but we do know the result appears to be.
Who is writing the logic test, then? From the answer you've linked: I don't buy "it would be very embarrassing if more than a handful of solutions were flawed". For years corporations has been...
Who is writing the logic test, then? From the answer you've linked:
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.
I don't buy "it would be very embarrassing if more than a handful of solutions were flawed".
For years corporations has been lying to humanity and I don't see any embarrassment slowing down this process.
What they mean by "logic test" is that the LLMs are using formal proof engines like Lean. Maybe a more common example that people use more often is a type checker in a staticly typed programming...
What they mean by "logic test" is that the LLMs are using formal proof engines like Lean.
Maybe a more common example that people use more often is a type checker in a staticly typed programming language. The type checker ensures that the types in the program are well defined. Now, in this analogy, do note that the type checker is scoped only to the correctness of the types.
You can trust that if an LLM produces a program that compiles, that it does, well, compile and have logically consistent types. Now, yes, the program may not be correct, but again we're scoped only to the type correctness in this context.
My gut feeling is that a professional mathematician with this particular specialty has a better understanding of both the social and technical structure of mathematics than laymen like us.
My gut feeling is that a professional mathematician with this particular specialty has a better understanding of both the social and technical structure of mathematics than laymen like us.
The logic test is a small and battle-hardened piece of software whose job it is to check proofs for logical correctness. It is possible for it to be wrong. People occasionally find ways to prove...
Who is writing the logic test, then?
The logic test is a small and battle-hardened piece of software whose job it is to check proofs for logical correctness.
It is possible for it to be wrong. People occasionally find ways to prove contradictions. It doesn't happen very often, and the proofs are usually pretty contrived. You are not likely to just stumble into proving a contradiction.
I'm going to trust the mathematicians, who seem to believe these proofs are correct, but aren't these models a nearly perfect way to accidentally come up with proofs so contrived that they do...
It doesn't happen very often, and the proofs are usually pretty contrived. You are not likely to just stumble into proving a contradiction.
I'm going to trust the mathematicians, who seem to believe these proofs are correct, but aren't these models a nearly perfect way to accidentally come up with proofs so contrived that they do stumble into proving a contradiction?
Arguably yes, but it depends on how you use them. My understanding is that OpenAI told their agents to work out the proofs "by hand" first and then formalize the resulting proofs in Lean. I think...
aren't these models a nearly perfect way to accidentally come up with proofs so contrived that they do stumble into proving a contradiction?
Arguably yes, but it depends on how you use them. My understanding is that OpenAI told their agents to work out the proofs "by hand" first and then formalize the resulting proofs in Lean. I think that's much less likely to prove a contradiction than telling the agents to work out the proof in Lean and not stop until they prove the result (which they could achieve by proving a contradiction first).
Also, maybe I should clarify what I meant by "it is possible for it to be wrong". In theory, i.e., if the logic-checker is written correctly, then it is actually impossible for it to be wrong, in the sense of "if a proof passes the logic checker, then it is a valid proof". Whenever someone finds a way to prove a contradiction, that's a bug, and it gets fixed. Eventually, it will probably get to a place where it has no such bugs.
Thanks, I didn't know that. So in a nutshell we have a machine that can prove to another machine how to solve a problem... But people cannot understand the explanations the machines are talking...
Thanks, I didn't know that. So in a nutshell we have a machine that can prove to another machine how to solve a problem... But people cannot understand the explanations the machines are talking about.
Worth reading about the issue with big tech "solving" mathematics, long read: https://europeanreviewofbooks.com/the-spectacle-of-ai-taking-over-the-world/ Also a statement on the topic from...
Mathematical proofs are normally written as academic paper, typically in English with lots of equations. The equations aren't automatically checked. But more recently, they are sometimes...
Mathematical proofs are normally written as academic paper, typically in English with lots of equations. The equations aren't automatically checked.
But more recently, they are sometimes "formalized" by translating them into a specialized computer language. The most popular one is called Lean. These can be automatically checked. That will catch most mistakes. It's still possible that the Lean proof proves something different than what was intended, but it's much easier for a mathematician to verify that a Lean proof proves the right thing than to check an entire proof by hand.
Some of the proofs that OpenAI generated have a Lean proof. (Currently they are at 42%.) They are still working on them. OpenAi has already withdrawn a few proofs and also added Lean proofs for some others that didn't have one yet.
So verification is not done yet, but it looks like it will be done soon. Mathematicians expect that most of them will be valid, but we will see.
From the article:
[...]
[...]
[...]
This is honestly a pretty good way of putting it, in my opinion. One of the very last courses I took before graduating with a math degree just this year was a philosophy of math course. We were discussing what the impacts of AI on the mathematical profession would be more-or-less right when AI started getting good at math. I think the general consensus then was that the actual grinding out of proofs would fall to the machine, but the actual asking of questions and posing of conjectures (and understanding what we actually learned from conjectures being true or false!) was still solidly in the human realm.
Suffice to say, a very interesting time indeed right now!
This is quite something. I keep having the thought repeatedly: Another one (profession) bites the dust. Programmers, digital artists, animators, various analysts - business, economics, law..., now theoretical mathematicians.
And no, don't lie to yourself that AI is not and will never be good in any of this - we are long past the phase when it was good enough in many fields, now we are in the one when it is the best (and cheap) approach to many of them - as we see here.
Who will put food on our tables?
The writing is absolutely on the wall and news stories like the one I heard on the radio this morning "this just in AI is NOT taking our jobs" based on some report that it's slowing show how much we love plunging our heads in the sand.
Whatever the pace, our gerentocracy political class are demonstrating once again that they're not able to keep pace with the impact of changing times.
It's weird cause like, if your job is JUST pushing out code, then yea, AI is going to take your job. But the reality is many programmers write code for like 1/3rd of their time, and communicate across teams, managers, etc the other 2/3 of the time. Sure, AI replaces the code bit such that things that used to take weeks now take me hours to do, which means I could write more code but... the rest of the workflow still hasn't caught up, testing is still slow by nature unless we wanna give up and just have bugs in production like Github does. Planning is still slow, people still take a month to talk about shit before they make a ticket, etc.
Most of my day is spent sitting around and talking about "Do we even really want to do this feature?" or "Is this thing a customer reported actually a bug?" and maybe AI could do that if we told it to, but stakeholders don't want to talk to AI, they want to talk to the developer team. The architect leading the project is going to ask me about the code that I let the AI write and you better believe I'm expected to understand it. The companies that are letting AI just do everything have already found out the hard way that it leads to shitty software, looking at you, Github.
So, I think, while right now it seems like we need less developers, I think it'll end up like the cotton gin - there will be this really expensive task that's a part of the workflow that AI can't do, and we'll hire "developers" who are really just "code managers" who can do that task of being the Subject Matter Expert of the code they let the AI write.
And you don't think AI will be able to handle that eventually? It's currently being given the ability to do all the basic tasks. But what happens when it learns how to manage projects (semi- and then fully) autonomously? Nearly every time I hear someone describe reasons AI isn't taking any jobs, it seems to be reasons current AI isn't currently taking (m)any jobs.
The writing is on the wall.
Yeah I mean, maybe? But the thing is that people like being in charge. They like managing their own projects. They like talking to other people who manage other projects.
Like, fast food restaurants still have counters and drive thrus even though we’ve had the technology to replace those things for at least 20 years and it’s been commonly used for about the last 10 years. Most people prefer the self checkout, but the human option still exists for those who need custom service for accessibility reasons or whatever else.
It’ll end up like, if AI can manage projects, you’ll just have 1 project manager managing like 50 projects at once instead of ~5 that they can do now. We’ll still have the same number of everyone, but they’ll produce way more way faster.
That's because the human option is super cheap. Businesses will automate away as much as they reasonably can, plus a bit more.
I am sorry if I am making a stupid question. This is not my field and maybe I am naive... But if no one understands the proof how can we know it is valid?
I think @evergoe comment in the other thread helped explain this. Basically the proofs are written in a machine-checkable form and they passes the logic test. Human still need to check if those versions are actually congruent to the original problems but at least one barrier has cleared.
To get a better sense of how messy the situation is, see also this preprint:
In particular, this preprint alleges that while the result for Navier-Stokes appears to be correct (i.e. the lean proof does in fact prove the right claim), OpenAI's paper does not match the lean proof. So in this case, we do not actually know whether the paper proof is correct, but we do know the result appears to be.
Who is writing the logic test, then? From the answer you've linked:
I don't buy "it would be very embarrassing if more than a handful of solutions were flawed".
For years corporations has been lying to humanity and I don't see any embarrassment slowing down this process.
What they mean by "logic test" is that the LLMs are using formal proof engines like Lean.
Maybe a more common example that people use more often is a type checker in a staticly typed programming language. The type checker ensures that the types in the program are well defined. Now, in this analogy, do note that the type checker is scoped only to the correctness of the types.
You can trust that if an LLM produces a program that compiles, that it does, well, compile and have logically consistent types. Now, yes, the program may not be correct, but again we're scoped only to the type correctness in this context.
My gut feeling is that a professional mathematician with this particular specialty has a better understanding of both the social and technical structure of mathematics than laymen like us.
The logic test is a small and battle-hardened piece of software whose job it is to check proofs for logical correctness.
It is possible for it to be wrong. People occasionally find ways to prove contradictions. It doesn't happen very often, and the proofs are usually pretty contrived. You are not likely to just stumble into proving a contradiction.
I'm going to trust the mathematicians, who seem to believe these proofs are correct, but aren't these models a nearly perfect way to accidentally come up with proofs so contrived that they do stumble into proving a contradiction?
Arguably yes, but it depends on how you use them. My understanding is that OpenAI told their agents to work out the proofs "by hand" first and then formalize the resulting proofs in Lean. I think that's much less likely to prove a contradiction than telling the agents to work out the proof in Lean and not stop until they prove the result (which they could achieve by proving a contradiction first).
Also, maybe I should clarify what I meant by "it is possible for it to be wrong". In theory, i.e., if the logic-checker is written correctly, then it is actually impossible for it to be wrong, in the sense of "if a proof passes the logic checker, then it is a valid proof". Whenever someone finds a way to prove a contradiction, that's a bug, and it gets fixed. Eventually, it will probably get to a place where it has no such bugs.
Thanks, I didn't know that. So in a nutshell we have a machine that can prove to another machine how to solve a problem... But people cannot understand the explanations the machines are talking about.
... It seems surreal, somehow.
Worth reading about the issue with big tech "solving" mathematics, long read: https://europeanreviewofbooks.com/the-spectacle-of-ai-taking-over-the-world/
Also a statement on the topic from Association for Human Mathematics:
https://www.ahmath.org/statements
Mathematical proofs are normally written as academic paper, typically in English with lots of equations. The equations aren't automatically checked.
But more recently, they are sometimes "formalized" by translating them into a specialized computer language. The most popular one is called Lean. These can be automatically checked. That will catch most mistakes. It's still possible that the Lean proof proves something different than what was intended, but it's much easier for a mathematician to verify that a Lean proof proves the right thing than to check an entire proof by hand.
Some of the proofs that OpenAI generated have a Lean proof. (Currently they are at 42%.) They are still working on them. OpenAi has already withdrawn a few proofs and also added Lean proofs for some others that didn't have one yet.
So verification is not done yet, but it looks like it will be done soon. Mathematicians expect that most of them will be valid, but we will see.