What I'm feeling is that there's a need to study how to use AI well. I've seen professors using AI, and it was amazing. In that sense, I think AI prompt input will become stratified. In the past, implementation skills were very important, but these days, concepts feel more important this is one of those things.
It's not that AI brings equality, but rather that the output varies depending on how much background knowledge you have. You could call it a stratification of input
I'm starting to feel like there's no place left for programmers like me who focus on quickly churning out MVPs.
- Hasn't been peer reviewed yet, so take with a grain of salt. This applies to all claimed proofs, not just AI-generated ones. Even humans hallucinate proofs too!
- The prompt is on page 27 here[1]. It is ten pages of advanced mathematics priming the model in the right direction, apparently informed by a year of prior research. That doesn't invalidate the result if it is genuine, but it is worth noting that this wasn't a matter of "ChatGPT, solve this unsolved problem. Make no mistakes." and required substantial domain expertise and human research beforehand.
Crazy how intelligence is cheap, efficient and commonplace now.
We humans better refocusing our energy on our core values/principles, given most of our skills are becoming irrelevant
> I don't think researchers in math/TCS will be made obsolete, but I think it will instead no longer make sense to work on any low-hanging, or even medium-hanging (you know what I mean) fruit. We'll be needed for problems where actual novel approaches are needed.
I wonder how this compares to what we see happening with "juniors" in software development?
In math research, do you also get the training for the profession from working on the low hanging fruits for a while, to then move to the medium-hanging, and later go on to work on previously unsolved stuff?
I would agree with your take. I (author of the post & paper) learned a ton from working on small parts of problems my PhD advisor was doing a lot of the heavy lifting on, and later also from getting some results that were essentially putting together the right pieces that already existed followed by some deep-in-the-weeds analysis.
Except solving problem is probably the least (even though it's important) interesting thing in research...
The most interesting thing in research is finding new questions, that we understand and that we know why they are important. And that's something that humans need to do (by definition)
If I recall correctly there was a proposed proof to the abc conjecture by Mochizuki https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs which was rejected due to being rather inpenetrable to humans. Shouldn't this be an ideal target for LLMs?
There was recently an announcement that a group trying to formalize it found a gap exactly where other mathematicians were pointing. So to the extent there was any doubt, it should be gone now--the proof was incorrect.
But I agree LLMs have a lot of potential for checking proofs--both informally (they can read quickly and find gaps) and formally (by attempting to formalize).
I know a bit about this field. This conjecture reads as somewhat more niche than the cyclic double cover conjecture recently proved by OpenAI, but nevertheless represents a real contribution.
You want to know how long it takes to solve an optimization problem, in this case over convex, lipschitz functions. (The restriction to a spherical domain is not really a restriction, you can just change variables for any bounded domain.) Anyway, showing upper bounds on time complexity is "easy" because it's just the runtime of your algorithm. Showing (nontrivial) lower bounds is usually much harder because it requires constraining all algorithms.
This proof apparently shows that the lower bound time complexity is equal to the time complexity of an existing 30-year old algorithm: it requires Omega(d^2) function evaluations to solve over this class of functions.
My gut says likely implies that d is the minimal number of evaluations if you have a gradient oracle because you can approximate a gradient with d function evaluations, but I'm not sure how hard it is to make that rigorous.
Yes, order d is the minimal number of evaluations of gradients needed for the same problem! That has actually been known since 1979 (Nemirovsky and Yudin showed that), and there are methods with the same complexity so this question in the gradient model has been solved for a long time. "because you can approximate a gradient with d function evaluations" was exactly why d^2 made sense as a lower bound for this case! Basically, the lower bound question can also be thought about as "can you do better than approxing a gradient?", so this result says no.
Genuine question: If you still or did think LLMs are just stochastic parrots that just summarize everything and have no form of creativity, what do you think after seeing results like this?
I'm very curious how people reconcile their fear/hatred of AI with actual objective reality. This is actually what interests me most about the whole AI thing. How we tell ourselves what we tell ourselves.
They aren’t really stochastic parrots, they’re next token prediction machines. They aren’t intelligent nor creative imo. However they are quite useful at some tasks. Why would you assume people who don’t kneel at the alter of AI are somehow fearful or hate AI? Most of the hate I’ve seen have been for the people and companies involved with AI not the technology itself.
Like, this is just so silly. Come with me for a little thought experiment.
Picture in front of you a Kibana dashboard. It displays, say, latencies.
Now apply some statistic functions. Let's find the time ranges where we had outlier tail latencies, for example.
You pin down some patterns, cool. But this is post-incident. We want to alert on-incident.
So you begin writing some rules. And then some more rules. And then even more rules. All of a sudden you captured the entire logic of the program emitting these metrics, along with the surrounding dependencies'.
See where I'm going with this? To do sufficiently well at prediction, you'll need to model the entire constitution of the thing you're trying to predict, along with the stuff going through it. Locally, all predictions will be unlikely. But globally, you'll be right.
But if you do that, you quite literally "understand" and simulate the entire thing. That's the whole point, and this is why "just predicting the next token", "stochastic parrot" and other anti-AI dogwhistles are so flagrantly asinine. They imply some sort of rudimentary Markov process, or at best some sort of dozen or so variable statistics research paper type prediction. It's a laughable proposition, given the quite literally trillions of parameters actually in use, and all the research that has already went into identifying countless semantically interpretable latent spaces and activation patterns.
> Most of the hate I’ve seen have been for the people and companies involved with AI not the technology itself.
Anecdotes are fun! Visit any Reddit thread where AI is brought up and watch that ratio shift very rapidly. The hate and cope train is incessant there.
In the Reddit post there was clarification that this was done with Sol Pro not Ultra - curious what is everyone’s mental model of the difference.
My understanding is that ChatGPT Pro is effectively a multi agent system, or somehow uses multiple LLMs in parallel and selects a best answer. And Ultra is more similar to Claude-Code UltraCode where the main agent can choose to create a dynamic JS workflow that deterministically orchestrates multiple agents to handle different parts of a task and have adversarial checkers etc.
Is that more or less the difference? Any substantiating sources would be great to see.
This is all a depressing and bleak future that I don’t look forward to.
One solution is to ban LLM’s, to artificially create a demand for human thought, that just feels like living in an artificially constructed zoo.
Another solution is humans don’t do anything that AI can do better , / doesn’t need the human touch. So I suppose we will all become artists, sportsmen or politicians, the only jobs that will remain except for select few. Maybe this is ok, I don’t know.
Another solution is we find a way to mind-meld with AI so that human + Ai >> AI alone. This is dystopian, who gets to decide who mind melds with AI, how much will it cost etc etc.
For the stupid copes that the prompt required human ingenuity, let me first add that the author used GPT5.6 to write most of the prompt. He just gave some mild direction. That amount of direction does not require deep expertise and the expertise required will keep falling with time, eventually an undergrad can create this loop and then maybe a high school student.
And prompt engineering / loop engineering nonsense is not real. Calling it engineering is a psy-op because it is something simple, imprecise and future models will be much better at it than you.
In fact, in the future the most likely outcome is you tell the agent what you want (I want this app, or I want this theorem solved) and it will set up the loop, or loop of loops and use all its computing effort to come up with a result. This is completely dystopian to a human life.
could machine-learning even handle a TEN PAGE PROMPT just a year ago?
this is changing my mind, at least about experts using advanced tools like any profession where it's like the magic of watching a lifetime of hard-earned skill at work
> After seeing OpenAI’s CDC result, I wrote a much more elaborate prompt following the same general methodology. My prompt is about ten pages long and attached at the end of the preprint (see collection of links below). There is a lot baked into this prompt, on approaches to try and also on how exactly the model should proceed, but it's built exactly in the style of OpenAI's CDC prompt. One note is that I gave it a relatively small error requirement, to prove the quadratic lower bound under order d⁻⁴ accuracy.
> After 148 minutes, GPT-5.6 Sol Pro returned a proposed proof resolving the quadratic dimension dependence at accuracy of order d⁻³. After checking things myself, I formally verified the proof in Lean, and it passed the formal verification check.
I tried using AI to solve some advanced math problems. One thing I see is that they can throw an enormous amount of brute force into a problem. When mathematical logic can be brute forced we will see some interesting advances.
45 comments
[ 0.23 ms ] story [ 39.1 ms ] threadIt's not that AI brings equality, but rather that the output varies depending on how much background knowledge you have. You could call it a stratification of input
I'm starting to feel like there's no place left for programmers like me who focus on quickly churning out MVPs.
- Hasn't been peer reviewed yet, so take with a grain of salt. This applies to all claimed proofs, not just AI-generated ones. Even humans hallucinate proofs too!
- The prompt is on page 27 here[1]. It is ten pages of advanced mathematics priming the model in the right direction, apparently informed by a year of prior research. That doesn't invalidate the result if it is genuine, but it is worth noting that this wasn't a matter of "ChatGPT, solve this unsolved problem. Make no mistakes." and required substantial domain expertise and human research beforehand.
[1]https://arxiv.org/pdf/2607.13335
I wonder how this compares to what we see happening with "juniors" in software development? In math research, do you also get the training for the profession from working on the low hanging fruits for a while, to then move to the medium-hanging, and later go on to work on previously unsolved stuff?
The most interesting thing in research is finding new questions, that we understand and that we know why they are important. And that's something that humans need to do (by definition)
But I agree LLMs have a lot of potential for checking proofs--both informally (they can read quickly and find gaps) and formally (by attempting to formalize).
You want to know how long it takes to solve an optimization problem, in this case over convex, lipschitz functions. (The restriction to a spherical domain is not really a restriction, you can just change variables for any bounded domain.) Anyway, showing upper bounds on time complexity is "easy" because it's just the runtime of your algorithm. Showing (nontrivial) lower bounds is usually much harder because it requires constraining all algorithms.
This proof apparently shows that the lower bound time complexity is equal to the time complexity of an existing 30-year old algorithm: it requires Omega(d^2) function evaluations to solve over this class of functions.
My gut says likely implies that d is the minimal number of evaluations if you have a gradient oracle because you can approximate a gradient with d function evaluations, but I'm not sure how hard it is to make that rigorous.
I'm very curious how people reconcile their fear/hatred of AI with actual objective reality. This is actually what interests me most about the whole AI thing. How we tell ourselves what we tell ourselves.
Like, this is just so silly. Come with me for a little thought experiment.
Picture in front of you a Kibana dashboard. It displays, say, latencies.
Now apply some statistic functions. Let's find the time ranges where we had outlier tail latencies, for example.
You pin down some patterns, cool. But this is post-incident. We want to alert on-incident.
So you begin writing some rules. And then some more rules. And then even more rules. All of a sudden you captured the entire logic of the program emitting these metrics, along with the surrounding dependencies'.
See where I'm going with this? To do sufficiently well at prediction, you'll need to model the entire constitution of the thing you're trying to predict, along with the stuff going through it. Locally, all predictions will be unlikely. But globally, you'll be right.
But if you do that, you quite literally "understand" and simulate the entire thing. That's the whole point, and this is why "just predicting the next token", "stochastic parrot" and other anti-AI dogwhistles are so flagrantly asinine. They imply some sort of rudimentary Markov process, or at best some sort of dozen or so variable statistics research paper type prediction. It's a laughable proposition, given the quite literally trillions of parameters actually in use, and all the research that has already went into identifying countless semantically interpretable latent spaces and activation patterns.
> Most of the hate I’ve seen have been for the people and companies involved with AI not the technology itself.
Anecdotes are fun! Visit any Reddit thread where AI is brought up and watch that ratio shift very rapidly. The hate and cope train is incessant there.
My understanding is that ChatGPT Pro is effectively a multi agent system, or somehow uses multiple LLMs in parallel and selects a best answer. And Ultra is more similar to Claude-Code UltraCode where the main agent can choose to create a dynamic JS workflow that deterministically orchestrates multiple agents to handle different parts of a task and have adversarial checkers etc.
Is that more or less the difference? Any substantiating sources would be great to see.
One solution is to ban LLM’s, to artificially create a demand for human thought, that just feels like living in an artificially constructed zoo.
Another solution is humans don’t do anything that AI can do better , / doesn’t need the human touch. So I suppose we will all become artists, sportsmen or politicians, the only jobs that will remain except for select few. Maybe this is ok, I don’t know.
Another solution is we find a way to mind-meld with AI so that human + Ai >> AI alone. This is dystopian, who gets to decide who mind melds with AI, how much will it cost etc etc.
For the stupid copes that the prompt required human ingenuity, let me first add that the author used GPT5.6 to write most of the prompt. He just gave some mild direction. That amount of direction does not require deep expertise and the expertise required will keep falling with time, eventually an undergrad can create this loop and then maybe a high school student.
In fact, in the future the most likely outcome is you tell the agent what you want (I want this app, or I want this theorem solved) and it will set up the loop, or loop of loops and use all its computing effort to come up with a result. This is completely dystopian to a human life.I’m convinced many of you barely go outside and have the capacity for original thoughts.
Sloppity slop slop.
Should I ban table saws because they make people too good at woodworking? Should we ban right-angles?
This line of thought doesn't lead anywhere fruitful.
Or, for the vast majority of humanity who aren't professional mathematicians, it's a liberating and empowering advancement.
I'm sorry if the automated digital theorem looms are eliminating the market for your handwoven proofs.
this is changing my mind, at least about experts using advanced tools like any profession where it's like the magic of watching a lifetime of hard-earned skill at work
> After seeing OpenAI’s CDC result, I wrote a much more elaborate prompt following the same general methodology. My prompt is about ten pages long and attached at the end of the preprint (see collection of links below). There is a lot baked into this prompt, on approaches to try and also on how exactly the model should proceed, but it's built exactly in the style of OpenAI's CDC prompt. One note is that I gave it a relatively small error requirement, to prove the quadratic lower bound under order d⁻⁴ accuracy.
> After 148 minutes, GPT-5.6 Sol Pro returned a proposed proof resolving the quadratic dimension dependence at accuracy of order d⁻³. After checking things myself, I formally verified the proof in Lean, and it passed the formal verification check.