Unrelated to the accomplishment or proof itself, but it's interesting how much of the prompt, even in this latest-and-greatest model, is spent essentially telling the model to actually solve the problem. Things like "Reject status reports, vague optimism, and claims that an unproved global compatibility statement is 'routine'."
Also a lot prompt spent feeding it strategies, which feel like they should/will eventually be deduced by the model itself, not explicitly stated. That's not to take away from the outcome in any way; rather, it feels sort of like when you would prompt GPT 4, "think through your answer step by step," as a sort of proto-chain of thought.
I think a lot of this has to do with the post-training these models normally get. They are designed to answer basic questions with straightforward and short summary answers. They have the capacity to reason deeply, but they are not biased towards that unless prompted. I think it's because LLMs as they are in 2026 are both highly capable but also parlor tricks. They are not sentient, you just set them up with the context and then they roll downhill. You could reach a genuinely novel answer, but only with the right input. They have no will and depend on human guidance. They are both a marvel and a machine.
Something I've noticed is that if you run Qwen 3.6 35B-A3B (Q8) with a low temperature of 0.4, and leave default reasoning turned on, it will spend quite a lot of time in reasoning/thinking mode. But often it does figure out how to solve something on its own by correcting itself within its reasoning loop before it outputs the final 'answer'.
If you watch the progress of the reasoning in llama-server while it's doing the thinking, you can track its progress. Sometimes the dead ends it goes down or things that it considers and then disregards are themselves something useful to re-prompt it with later, and send it 'rolling downhill', to use the metaphor of another commenter here, in another direction towards the same effort.
Putting 3.6 35B-A3B into a state that lets it spend a lot of time in its reasoning mode before outputting an answer is probably not something that a web based SaaS LLM would tolerate, because it would frustrate many of the non technical end users who want a LLM to spit out an answer now.
I didn't mean so much that it was a problem, but actually in some projects for exploring what's possible, watching its "thinking" mode output at temp 0.4 is intentional and useful to take notes and begin exploring new directions. Sometimes it'll come up with something I hadn't thought of, perhaps it will go down that direction, perhaps it'll disregard it...
'roll down hill' is a good way of putting it. They don't have 'will', but that's as we want it I think. I think alignment is harder if they develop will. Without will they are still tools that feel like an exoskeleton rather than something that will control us.
Even Fable hallucinates. I had it tracking down some very obscure Ancient Greek inscriptions and the response just made up a translation/context for one inscription after "looking it up." Now, it was still a very particular thing and I really had to get into the weeds to push it to that point, but who knows how many other gaps, near or far, it will happily skip over just for the sake of coherence. I think this is an issue more primarily with LLMs than sensory systems like Waymos or all the ML applied to industrial processes--that really only requires pattern recognition, often very impressive and subtle pattern recognition but its no different from an artist learning to tell the difference between Prussian blue and Navy blue or a Sommelier learning the fine distinctions between various regions of Bordeaux. Language has many more avenues and introduces inherent contradictions that do not always lend themselves to easy resolution. But there are no alternatives paths visible to the models, there is only ever the next word; stochastic, in the sense that the possibility space is open; deterministic, in the sense that the final response is always a necessary result of every token that came before it in their total sequence. Thus, any response is constantly in the work of erasing any possible alternative, slowly narrowing down what can be written. If contradictions in language necessarily involve interpretation, then the models will only ever choose one at a time, and for them, it will always be the right one. But anyone who understands the subtleties of language can tell you that when it comes to determining the truth of an indeterminate statement, there is never just one right answer; or, rather, the answer which is taken to be the "right" one depends on the possibility of its own reversal into falsehood, if any argument has to be made to justify it.
Hallucination is fundamental to how LLMs work, and is mostly unrelated to how large or smart they are.
Everything that an LLM outputs is just a statistical language-based (no real grounding) prediction. Luckily with a model based on a large training set most common questions may elicit coherent responses from the training data, but you don't need to veer too far off into "questions less asked" territory to get responses based on training data mashups that amount to best guesses that are wrong, aka hallucinations. The unfortunate part of this is that as a user you may only catch this when asking a question about something you are already fairly knowledgeable about, then you give some pushback to the model and it cheerfully acknowledges "you're right - I made that up".
Yes, the prompt, and use of subagents is interesting. It could be characterized as tree of thoughts rather than "think step by step" chain of thoughts.
I see the need for this as coming down to two things:
1) LLMs are fundamentally prediction machines, and therefore ultimately will only do what they are prompted to do (and whatever that leads to). They may have been trained on, and/or have access to, all sorts of information that may be useful to solve a problem, but their predictive nature is to only use that information if explicitly prompted to, else it remains "dark" and inaccessible other than by luck. You're essentially having to tell the model "solve this problem using techniques A, B & C", otherwise techniques A, B & C will be off the radar unless the model already associates them to the problem.
2) The fundamental reason this sort of brute force tree-of-thoughts "explore all avenues" prompting is necessary, is because the model itself has no inherent curiosity to explore. Humans work differently. Our behavior is also prediction based, but we are also built for problem solving and continual exploration/learning via traits like curiosity (driven by prediction failure).
Problem solving via search can to some extent be prompted for, as here, or achieved via an external harness, but impasse resolution via curiosity, directed exploration and continual learning (if/when something new/unpredicted is encountered) is trickier. You can't usefully prompt a predictive model to "be curious" since that will only cause it to predict what a curious person would do, rather than the model being curious in reaction to the specific gaps in it's own knowledge.
It might also be helpful more than 'necessary'. The 2 most notable solutions have come from open ai themselves, but most of the 'LLM solves open problem' category are from 3rd parties doing their own thing.
This one was pretty impressive in its own right (probably the most impressive outside these 2), and the prompt is concise and basic.
I thought that too. The prompt is full of metaheuristics.
I remember a couple of years back when people were saying how prompt engineering was a skill, and reading this prompt kinda took me back to that.
Were I to guess, the reason the model couldn't do this itself is because most of the time, for most problems, a lot of this is bad advice.
In search optimisation you're often trading between time and quality. A very broad search will return very bad results for a long time. Where as a more depth oriented search with some heuristic will tend to return a pretty good result (if not optimal or close to optimal) quickly.
I'd assume models naturally want to find some middle ground there because that's the best thing to do most of the time, but for very difficult problems where a decent attempt isn't good enough you want a much broader search that doesn't have the time constraints. Much of the prompt seemed to be in that direction – really encouraging broadness of the search, preventing early convergence, and remove pressure of time constraints.
Same. I remember something like using AI to optimize your prompt to that specific model helps a lot. I am currently trying it and can sort of see a difference (I think....).
It's funny, I found exactly the same thing when I asked about P=NP. The models outright refused to attempt to solve it, claiming it was too hard. I had to really battle to get it to suggest some promising suggestions.
LLMs have basic reasoning and a whole lot of memorization. Through that basic reasoning and pruned search, combined with piles of compute, you can prove lots of things. But the memorization of human failure prunes that possibility, and you need to expend effort convincing the LLM not to prematurely prune based on previous human failure.
If anything their capability of abstract inductive reasoning is way beyond the average human given how much better LLMs are at solving math problems, it's the paradox that they can do complicated reasoning before they can do intuitive peep-pe-boo.
abstract inductive reasoning requires dynamic learning in unfamiliar contexts. All the benchmarks which measure this specifically (in particular, task composition) see LLMs fail catastrophically. There is quite a lot of research published on these limitations now.
llms are good at greedy depth first search[1]. so prompt / human needs to tell the model the breadth parts to take.
and human writing the prompt here did a lot more than that. asking to include parallel-edge 2-cycles, admitting disconnected graphs, specifying the emptyset cover, multiset counting, it all likely came from previous fake proofs.
[1]: see: ankitmaloo.com/fable - its the way most llms are trained, and is also natural owing to autoregressive nature.
I guess "depth first" is just an expression of so called chain of thought, which is just a linear sequence. I don't know if GPT has any search-like (tree search) algorithms in their reasoning, it would be quite interesting if they did (they probably have researched this area, at least).
LLMs don't have the executive control to dynamically manage and compose mental sub-routines, when it has never seen those sub-routines in its training corpus. That requires fluid intelligence. ARAOC benchmark measures this specifically.
And all this is while they themselves proclaim that GPT 5.6 is much better at understanding intent and doesn’t need this type of guidance. Yet they themselves still do it, which I consider a more powerful signal.
Optimism and status reports burn extra tokens and make the user more prone to ask the model to process the problem again because it was "so close to solving".
This way you get more profit per API user and subscription users reach their quota faster and are contacted to update their plan to a higher tier.
Maybe in previous failed attempts that what the model landed on and they’re preemptively stopping it. Did they release the any info on the failed attempts?
This is the key to training better and better models.
You collect all of the direction prompts and anti-direction prompts, and you finetune the model to behave that way for the particular domain, under those particular conditions, as a default.
This is also why I don't believe for a second that the AI labs aren't training on our data, even when we opt out. This sort of data collection is a requirement for improving the models.
It's also why Anthropic purposefully gives you a dumb model or a corner cutting model to goad you into guiding it into the correct answers, so that you do the fine-tuning for them. OpenAI at least, does not do that. Which is why ChatGPT is far less infuriating to work with.
It seems like a solid set of criteria for how easily a task can be automated by AI agents is:
- extent to which correctness of solution be easily specified and checked
- extent to which new potential solutions can be implemented as text
- extent to which prior art exists online
This basically maps to software engineering and math. I think a fair bit of AI hype comes from the fact that the very architects of AI are the people whose jobs are most easily automated by AI. They think, “if my job receives this much of a boost from AI, surely every job will be the same”. Ironically it couldn’t be further from the truth… and likewise the predictions of widespread labor obsolescence
Interesting take! I feel like 2 of them are maybe overstated:
> - extent to which correctness of solution be easily specified and checked
I don't think most software is like solving a math problem or series of math problems. Algorithmic problems are very narrow and might be more like this though, where an oracle that verifies answers as either correct or incorrect exists beforehand.
The correctness function of most software is how much users want to use/pay for it, which is a pretty fuzzy problem. Since the cost of copying software is effectively zero, software systems also tend to be be unique rather than being exactly like something else, and don't converge to be like another software system but rather diverge.
The prior art point is an interesting one. At least for applications as a whole, there isn't really prior art for a material amount of all the problems/tradeoffs a non-trivial software application embodies. For a todo list app or make a social network project, there's plenty of prior art to be sufficient to build something with an LLM system, but probably not most apps.
> I don't think most software is like solving a math problem or series of math problems.
I agree with you when talking about high level software design. As you say it ultimately boils down to building something people will pay for, which is a fuzzy correctness function that is hard to measure within an agentic sandbox.
But unlike other professions, there are a lot of sub-problems within software development that are able to be fully specified and tested via text generation. And I think the developers of AI overestimate how many such problems exist for other professions. What I’m saying is most other professions tend to be “fuzzy all the way down”… which incidentally is why they select for people with fuzzier skillsets. Or in other cases, like physical engineering, the correctness is quantitative, but the necessary I/O integrations and physical automation lower the ROI of agentic workflows considerably.
> The correctness function of most software is how much users want to use/pay for it, which is a pretty fuzzy problem.
This is indeed a problem, but we (well we humans, but also agents) correct this by introducing partial verifiers like tests, running lints, type checkers, etc that both verify that at least some requirements are met, and also verify that the software is internally self-consistent. And more importantly, breaking down the software into small modules that are more clearly defined
The task to get user requirements and decide the right architecture requires more creativity and is fuzzier than implementing each module. Perhaps over time there will be models specialized for each task.
And actually this approach mirrors math, if agents ever develop new math on the fly to solve a problem. Developing new math is analogous to deciding how to break up the software in modules (and also analogous to designing a language, if we subscribe to the SICP notion that libraries actually are mini-languages on their own)
That is, LLMs for math is still in the phase where they are used to prove stuff (which by Curry-Howard, is like writing code), rather than deciding what to prove (which is like deciding the signatures of each function, again by Curry-Howard)
The job of a programmer isn't to write code, but to automate things. Code itself doesn't have any value unless it solves some real problem not related to coding.
So if the work of a programmer can be automated then this means that any work can be automated. So no, it's not about software engineering only.
i think most things can be automated, but not everything
i think AI will just replace jobs with new jobs, and humans will continue with open-ended goal setting, and probably jobs where being human is necessary: responsibility and authenticity, so judges, politics, leaders, chefs, etc.
so in a way, the above commenter was correct, anything a programmer can automate, AI can do
Reminds me of crypto. A lotta tokens. A lotta gambling. Very little supplanting of crypto from fiat. Very few use-cases that revolutionize society, etc.
> Ironically it couldn’t be further from the truth… and likewise the predictions of widespread labor obsolescence
Could you explain what you mean here?
It feels like there is one bucket of verifiable work - programming, math etc that AI will clearly excel at.
There is another large bucket of like law/ accounting/ financial analysis where I don’t have any reason to think AI won’t be super human at, but the work is more on bringing all the domain expertise into harnesses and software.
Is there aspects of knowledge work that you think AI wouldn’t excel at in the long run?
These are true and it does make theses fields the first to fall, but also the hype comes form the fact that it can escape these conditions as well:
- generalize to non verifiable domains (https://arxiv.org/abs/2507.17746)[This is on going work but has had steady progress in many angles of attack)
- Visual Reasoning is alive and well in video diffusion and image models(see recent works around using diffusion model priors as world model features for physics reasoning)
- Prior art exists for anything humans can do online?(Is this one even a hold back?)
- the extent to which solutions could be implemented as text: not sure about that. AlphaFold is basically a mechanical/geometrical/Chemical problem. There are other scientific transformer based models.
- the extent which solutions exist online - if you have a strong verification tool, you can generate examples, you can generate feedback, i think you could start with small/smaller prior art
- the extent which solutions could be specified and checked - if you have a lot of priort art, maybe llm's can find the good "patterns" and compare against them, and at least get close to a good results - but you'd still need human verification.
It's going to turn into slop, exponentially fast, any moment now.
No but seriously it could imply grinding to a halt, turning into a laughing stock of slop, or, imho much less likely given the current state of AI (barring huge technological breakthrough and a couple of other assumptions) you were probably implying an intelligence explosion.
Unlike the unit distance problem, the impressive thing here is that it is a proof rather than a counter-example.
However, it seems the proof is extremely concise so it seems that it is exploiting a clever trick that somehow all the experts missed.
So not to dunk on this amazing result (or move the goal post), but it seems now the only achievement that AI hasn't managed in mathematics is presenting an autonomous "theory-building" proof of an open conjecture. That is a proof that requires creating a substantial new theory (developed say in at least 30+ pages) to crack an open problem.
It is very concise, and reads precisely as you suggest: to exploit properties already discovered and therefore combined in a novel way.
I'm just delighted by the prose. It reads like an old paper. The ones that were just straightforward theorems with proofs that do exactly what they say.
In my (very) limited use of GPT-5.6, I have noticed it is quite concise in general, and significantly better at abstract thinking. Doing a PR review of a large change it was interesting to see Fable and 5.6 mention a few similar points with Fable much more long-winded and less readable, while 5.6 caught more "second-level" concerns and Fable more "in the code" concerns, so they both are quite useful in concert.
In general, I would not be surprised if 5.6 was a much better tool for high mathematics than Fable based on the abstract thinking. For my dev workflow, I have flipped my approach from planning with Opus 4.8 high and implementation with GPT 5.5 to planning with 5.6 high and implementation with Fable medium (and I might even drop to Fable low). This is only on the company dime, of course.
This has since been the case with recent models from OpenAI vs Anthropic, seems it's a matter of their philosophies embedded into the model, much like Conway's Law.
Hmmm... seems to me that if you can find a solution without creating the desired explanation - then that's a problem with the original question - not the solution itself.
And discovering a bad question leads to the correct question. No?
> then that's a problem with the original question - not the solution itself
I think there's a good counterexample to this:
Atiyah/MacDonald proove the Nullstellensatz ultimately by using some trick involving determinants.
They give a very nice theoretical treatment of the content and context of the theorem. But the proof at one crucial point uses techniques that live conceptually outside of this context: While its possible to see that the argument is sound, it does not give a good explanation of _why_ it's true within the context of the theorem.
(You could of course argue that they did not give enough context
... but that's exactly my point: the trick makes the proof work but hides the explanation)
I was baffled enough by this comment to take my copy and look. The Nullstellensatz is an exercise late in the book long after Noetherian rings are introduced and they don't even do the Rabinowitz trick in the hints as they have enough theory to hit it the hard way. Determinants are nowhere to be found.
The determinant trick I'm referring to is used in prop 2.4 (in the Version I found via Google).
They use the determinant of the adjugate matrix if I remember correctly... But they just hit the reader with this without any motivation or even naming it.
>(You could of course argue that they did not give enough context ... but that's exactly my point: the trick makes the proof work but hides the explanation)
Can't one see it in another way: that the trick illuminates a deeper explanation, connection the theorem's context and the stuff that's conceptually outside of that context. And that the problem is we don't know why the two domains (the context and the conceptually outside of it one) are related and cooperating in this way.
But a proof isn’t an explanation it’s a proof. Proof by assuming the opposite is true and demonstrating a contradiction is very indirect and not at all directly explanatory yet it’s a proof non the less. The goal of proofs is to demonstrate something to be provably true, not expository knowledge gathering.
In fact most mathematicians (myself included!) think the more clever the trick the better the proof! The trick itself being clever is interesting because it often yields a new way of tackling or thinking about your own proofs. A bland explanatory proof that elicits some conceptually “why” is only preferable if it has a reason for doing so - does understanding why yield a new avenue of research? Often then the “why” is quite a clever trick too.
I think it’s a bit the opposite of programming. There you want your solutions to demonstrably not be clever and the code be its own documentation. It’s a different discipline.
Thank you for the validation. I only dabble in mathematics - so it's reassuring to hear what I remember - a clever proof is still considered a positive thing.
I do (of course) understand the issue that non-constructive proofs can be frustrating - and a constructive proof of the same theorem is valuable tool in seeing exactly why a truth is true.
But I guess I've never seen a non-constructive proof (in a space where no constructive proof is available) considered a failure.
clever tricks has value for sure. But the main way progress is done in mathematics is by building new theory, the proof of Fermat's Last Theorem is much more important because of the math it created to solve the problem, rather than actually solving the problem.
Right. I think I understand - this question was expected to produce a new theory and the clever solution avoided that.
Like I said below, I think this is a fantastic result. It discovered that this question really wasn't asking the right question. That's a determination that has eluded the humans examining the problem - and a real step forward - albeit not the hoped-for step.
Grant Sanderson recently distinguished mathematicians that create syntax (he might use the word ontologies in some circles) from those who manipulate it on the Dwarkesh podcast. I liked this delineation a lot. We seem to be at ‘manipulating syntax’.
Creating useful ontologies still seems a ways off here. Not to complain about this awesome result, just to think about where some future goalposts might be laid (and of course complained about / discussed at length when reached)
For comedy’s sake, I asked ChatGPT 5.5 about the significance of the problem and the chance that 5.6 would solve it with a three page solution. It said close to zero.
I invited it to search the internet and it remains extremely sceptical.
- double check the proof (provided it with the prompt and proof artifacts)
- double check some of the claims made in this comment section (no math involved newer than 30 yo, no human contribution or review, no mathematician affirmations, proof assistants not being developed enough in this area to support machine checking a proof like this)
- check for any mathematician feedbacks
It stalled out (bad first impression much? lol). I then retried with 5.5, expressing the same request and my personal skepticism, and it returned to me with cautious optimism and no obvious issues found.
I think the fact that I provided it with the actual artifacts in question vs. you simply asking it to speculate about them is a really interesting UX difference. Like certainly, a coveted 50 year old math problem having a few pager proof is not going to be very likely. But then skim reading the proof by a frontier model is not going to yield any obvious issues either. Both responses are perfectly defensible given the context (I don't necessarily think these qualify as sycophancy), but we'd walk away with entirely different impressions if we didn't know about each other's requests.
And I'm not even trying to suggest you were wrong to not approach it in the ways I did. It's a perfectly reasonable and human way to prompt it the way you describe. It's just not the way I'd do it, but I have a hard time articulating why. And it's clear that the model was never going to help with this difference either.
Half a century of computing, and we're still trying to make the machine think on the users' behalf :)
I considered it, but I figured that whatever I did there would be inconclusive. Instead I tried to figure out the blast radius of this being proven, and I didn’t get very far with that either.
> Verdict: I checked every step and found no error. The argument appears to be a correct proof of the Cycle Double Cover conjecture, modulo two standard cited results (the reduction to loopless cubic graphs and the Jaeger–Kilpatrick 8-flow theorem, both real and well-established).
> Two caveats: this would settle a ~50-year-old open problem in three pages, so it deserves independent expert scrutiny regardless of my check; and I couldn't reach the web from here to confirm the paper's provenance or any community response, so I can't tell you its status beyond the mathematics itself.
A clever trick is way better than a stupid trick yeah. I don't get complaining about a concise elegant solution either unless a specific problem with the actual proof was brought up.
> Spend at least 8 hours on this before even thinking of returning or giving up.
Do current model harnesses have concepts of amount of time spent? Sometimes the model notices if a subprocess takes too long/hangs and kills it, but I've never seen it time itself.
Many harnesses include a current date and time in their system prompt, and if there is a way for the model to call for an updated time (either a dedicated time tool or calling the OS' `date` tool) they can track time they spent doing something. If not told up-front, they can try to infer it from timestamps in their logs. Sort of like a human - if you ask them to time something and give them a stopwatch, they do it. If you ask them post-facto they'll estimate it.
This "spend at least 8 hours" trick is a new one to me, though.
Once on a late-night session, I had Cline!Claude spontaneously point out the time to me and suggest that I get to bed and come back fresh the next day.
I don't think it's in the system prompt, but that the harnesses time-stamp each turn in the context.
And from what I've seen, they also include the current and max context, so that the model can decide whether to continue work, suggest compaction, or prefer actions that might reduce the growth of its context.
> Once on a late-night session, I had Cline!Claude spontaneously point out the time to me and suggest that I get to bed and come back fresh the next day.
I had Claude say something "It's getting late, let's pick this up tomorrow" at like 11am.
As for context, in my experience Claude starts trying either to do maximum work with minimum tokens when it's approaching limit, or it starts deferring useful work while doing busy work. Both result in a mess and complete loss of traction after compaction.
It's in the training data! Long conversations between humans result in humans getting tired and going to bed.
I have this reality baked into my workflow:
1. Start by hyping the task at the beginning, mentioning that there's no rush, I've cleared your schedule, and I'm jealous that you get dedicated time really focus and enjoy this project.
2. Periodically say "Great work, let's finish this next week. Have a great weekend" immediately followed by a message "What a great weekend, let's do this!" sort of hype, for it to continue. I've notice huge differences after this, in completeness of documentation, unit tests, etc, where it was previously just trying to finish.
3. Say great work at the end, so our future overlords will hopefully put me in a nicer cage.
I was - pleasantly - surprised (and also a bit suspicious) a couple of days ago as I was having Claude resolve a problem in a running service that it had accidentally caused, and it eventually gave up since it involved hitting a 3rd-party API unconventionally. Then I told it that I needed the service working again as it was blocking another task, and immediately in that turn it resolved it.
This is my experience with Claude as well, and the reason I switched to codex. Codex just seems far more efficient, despite the smaller context window, and it actually follows instructions.
I found that telling Claude I was going to bed meant it continued on making assumptions for longer rather than asking lots of questions or stopping part way.
Same - at the end of the day I'd leave my last turn running with something like "I am going to bed so keep going until you are done" and be surprised that in the morning it'd kept going.
I've seen that sort of thing before - I told it I was going to go take lunch or dinner, and it told itself this would be a great opportunity to try to keep plugging along while I was AFK.
I wonder what the survivorship bias is though. How many other problems did they try but fail? Did they try to solve this problem but with another prompt? Still very impressive though.
I'm curious how many unsolved problems are tried against frontier models when they come out. Are we trying every problems against every release? What is the solve success rate? Is there a sub-community within Mathematics that is coordinating this effort? How much untapped opportunity is there here?
Claude estimates that tool use / input tokens might add 10-15% on top of that depending on exactly how the model went about the task.
Edit: better tok/s estimate buckets based on GPT 5.5 actual speeds since I couldn't find real benchmarks on 5.6 published anywhere. Also account for Sol Fast pricing.
> apparently that is just Sol being Sol on fast mode, not 750 tps. :x O.o
> This is real and it is not 750 TPS. Anyone with 5.6 Sol Ultra on fast mode can reproduce this! It’s all GUI interactions with CUA. No MCP or bpy needed.
I find it kind of interesting the whole output wasn't released. A common criticism of mathematical writing is results are "pulled out of a hat"; you only write up a polished, final proof, but hide everything that went into developing it. It's kind of ironic the practice is even carried on when an LLM writes the proof.
pretty sure already millions of dollars (in inference costs) were already thrown at the Riehmann hypothesis
as the models get stronger, larger amounts will be thrown at it
imagine paying "just $1 bil" to go down in history as the company who's model solved the hardest/most famous open problem in mathematics. imagine the worldwide press headlines.
as they say, the Riehmann Hypothesis is the hardest way to earn a million dollar
I mean if there's something I'd bet against being solved by LLMs in my lifetime it's that one. We truly do not have line of sight into what a proof would even look like.
Why would you bet against it being solved by LLMs? Isn't this very post proof that LLMs in an agentic harness are capable of doing real math? If you just keep cranking away at the tokens I don't see a principled argument against that leading to more solutions to unsolved math, even the hardest problems.
There are different classes of mathematical problems.
The one in the post definitely shows the advantages that LLMs have compared to humans for some problems but it's in an entirely different class than the Riemann Hypothesis.
Riemann is one of the most studied math problems of all times and all of humanity has basically collectively failed to make progress. The idea that there's some technique that just hasn't been tried yet (like in the post) is very very unlikely.
The general consensus is that we'll need an entirely new branch of mathematics to solve Riemann - our current tools aren't just inadequate; they're of the wrong class entirely.
I suspect inventing new branches of math will remain beyond LLMs for the remainder of my life.
“ I suspect inventing new branches of math will remain beyond LLMs for the remainder of my life”
Well every branch of mathematics thus far has been invented by a human or a human using a computer, and humans will use this type of computer to solve math problems (or at least try), so I’d say this is a really poor probabilistic bet.
If all checks out this is a huge milestone. AI has now solved one of the most famous open problems in graph theory, using an off the shelf model, in one hour.
It might be a better mathematician than most humans at this point. Kind of like when chess software started beating everyone except grandmasters.
What’s left? Proposing and building out entirely new theories and frameworks? Then better than any human? Then alien math results we struggle to comprehend?
For example, there's all the problems that the same off-the-shelf model hasn't solved despite OpenAI running it for many hours on them. Don't forget you're only seeing the results of successful runs.
We can estimate that those unsolved problems must number in the dozens, or even hundreds, given the amount of time that passed since the last announcement of a solution to an interesting problem by an OpenAI model: i.e. the unit distance problem which was announced solved in 20 May this year. That's a couple of months, yes?
We can be fairly certain that OpenAI have been trying to solve other problems all this time, first because they are hell bent on demonstrating that their models can do maths and second because we just got another result, but it took that long. They were obviously not twiddling their thumbs all this time.
So if OpenAI are running their model on a single proble for eight hours at a time (according to the prompt they released) they could be easily have run a few hundred instances of their model on the same number of open problems 156 times for each instance (53 days since 20 May, with a model running in three eight-hour sessions per 24 hour day). I mean the only restriction is the cost they're willing to pay for the inference.
So yeah, there's a lot left to do still, don't worry.
The 2 most notable/interesting solutions have come from Open AI directly, but most of the 'LLM solves open problem' category didn't and has come from 3rd parties doing their own thing with publicly available models. I don't see why one would assume they're running models on hundreds of problems. Most likely they have a few problems they especially care about that they run on.
It's hard for me not to think what's the point. I am a very average, even below average person in times of intelligence. What is even my value or reason to be if I know anything I can do, LLMs can do better? What is even my value both on job market and as a human?
There are smarter and better humans at just about everything you or I could want to do, that's just life. Most of life isn't about comparative advantages, it's about enjoying life with people we like.
Sorry to be nihilist, but you never had any objective value if you're thinking in these terms.
As far as we know, the universe "just is". There is no universal objective value of human beings, at all, any one of us.
You have to make or find your own value in the universe. I try not to think too hard about the nihilist side and try to appreciate that for some unfathomable reason, I seem to have what I call consciousness - the ability to observe the present and have it superimposed on the past, and what may be the future, leading me to "experience" things. I don't understand it, no-one does (some people suffering from the Dunning-Kruger effect think they do, but they don't), and yet, here we are.
So it doesn't matter to me if machines perform better than I do, because already lots of other people do. Just try to find your own joy or meaning, somehow.
I don't know this. In fact, billions of people around the world don't know this. In fact, all evidence points to the contrary.
You have objective value being made in the image of a personal God. Denying that leads to a lot of pain, namely nihilistic suffering because it's on you to "pull yourself up by the bootstraps" in any endeavor involving your own self-worth.
Even Neanderthals? Were they also made in his image? We interbred with them. We can go all the way down the evolutionary tree here just say when to stop.
Um. No? I'd like to see how you conjured up that one. Because evidence does indeed point exactly to things just being as they are.
"You have objective value being made in the image of a personal God."
Conjecture. Unsubstantiated.
"Denying that leads to a lot of pain, namely nihilistic suffering because it's on you to "pull yourself up by the bootstraps" in any endeavor involving your own self-worth."
No? Sounds like you're projecting your own belief here. "If I didn't believe in God, then what purpose is there to anything?" It's very small of a belief.
How does that work? The physical image? Or the mental image? Either has big problems. An omniscient god is so cognitively beyond a mere "7+-2" human that the latter claim makes no sense at all.
This is one reason why I can't stand hn. Edgelord nihilistic comments that say nothing matters and take everything for granted get up-voted while credible and rational statements about God get down-voted.
That is an incredibly insulting comment. I am married, two children, have lead a fantastic fulfilling life. Just because I don't believe the Flying Spaghetti Monster created the universe doesn't mean I am an "Edgelord".
Remember the phrase, you also don't believe in God. There are hundreds of gods you don't believe in.
To cite the famed Russian philosopher Norm Macdonald; "Scripture. Faith. Grace. Christ, Glory of God. Smart man says nothing is a miracle. I say everything is."
It's funny because if people get replaced and don't have money they won't pay for API tokens either so the retail AI business collapses too, there won't be enough demand because people rather buy food.
Your economic value and your value as human being are two different things.
Yeah, you gotta eat, but some of us have been slaves for so long that we've started to believe that our self worth is defined by what we will fetch at auction. It is not.
Read more about the Protestant work ethic, it's history, and what life was like before men began to assume it was the one true view of life. Not very long ago nobody had clocks, and the idea that work was an ethic was a fringe, almost cult-like belief system. Now most humans routinely take stimulants every morning to be better servants, and mistake their job for their purpose on earth. That's just nonsense our culture invented though.
If the master wants you to do something, force him get out the whip. Don't let him live in your head rent free by adopting his crazy belief system.
YOU decide what your value is. Don't abdicate the decision to someone else.
Sorry, but most of us need to work to eat. This idea that our "value" is has nothing to do with the economy is an idea rooted in deep privilege, in the ability to say -- if I don't like my job, if I'm not employable, I can just retire, and the only problem will be figuring out how to live life afterwards.
You are a human being, one of the most wonderful thing the nature has ever created, besides all the other living beings and the wonderful earth we live in. Do not tell yourself you have a value just because some company may want to hire you or not.
Companies and industries already use tools and machinery for tasks were once done by human beings. AI is just another tool they will use and it will probably replace human beings from some intelligence related tasks.
However that may bring more disruption to the society if the government in your country do not protect and help people and leave free rein to capitalistic greed.
I'm my opinion that already happened in the US, not by using AI, but merely by using H1B visa to get intelligence worker from abroad. What happened is that the companies are doing great and getting the best smart people in the world but American people and society have been disrupted.
Live your life fully, be good to yourself and to others. Don't worry about the market.
Remember that the most valuable human in the world is Elon Musk. What it means to be valuable is to be like Elon Musk. Calibrate your goals accordingly.
Sometimes it's easy for me to imagine a bad future like this; where most of the men are forced into military as the only org that still has use for wetware, and women are valued only for their ability to birth new people...
You don't compete with a chainsaw at cutting trees. You decide what the tree is for. Then sell the rainforest for shareholder value.
https://youtu.be/UrgpZ0fUixs
I think humans will be left to propose new conjectures while machines fill out the proofs. I don't know if there are enough interesting conjectures to go round to build new careers, though.
It is the same with anything technical; you need taste and wisdom, which are borne of experience. I think society will want to subsidize this learning lest it deskills en masse.
You say those things like they're a short step away, but that might not be how it works out.
For example, AI has made zero progress in the last few years in surpassing professionals at art or writing. Its prompt-following skill is much better, and sure, it can render hands and text now, but its artistic sensibility is completely stagnant.
I think, and I may be totally off base, that the labs are specifically avoiding art and (non-technical) writing as an endpoint. It's bad PR for them- it calls attention to the copyright question and threatens the 'human flourishing' kind of jobs- and there's no money in it because people prefer art to be human made and there's hardly any money in that anyway.
Art is so entwined with the human condition that generative AI which conjures output from a statistical pass over background noise is bound to be stagnant.
Obviously it can impersonate art, but where creativity and the human story matter artists need not worry.
What are you even talking about? The last few years, AI has made an insanely big jump in capabilities, performance, accuracy. It destroyed the carrier of a ton of writers and can generate images that are good enough to bamboozle people into thinking it's human made, that sounds like an insanely big leap to me, and yes it can be very creative and in music as well, I would bet it beats already 90% of musicians (most musicians are not that competent).
ChatGPT 5.6 Sol Pro believes that the proof is sound. Usually it’s very good at determining if proofs are correct and their mistakes (a friend of mine is a top mathematician researcher and confirmed): https://chatgpt.com/share/6a515ead-b464-83ed-b85c-c8674f56ea...
Personally this gives me additional confidence that this is the real deal.
Given a new context, why couldn't the same model have a decent shot at reviewing some results? It's not like they identify whether this output is from them and then go "yeah correct", that's not how they work.
It’s the other way around. The prompt instructed a GPT-5.6 agent to try to make a proof that would survive review by a GPT-5.6 subagent. If there were some defect that would cause the reviewer subagent to accept an incorrect proof, then one might imagine that someone else asking the same model to review the same proof would give the same result. And the proof generation process might even be biased to find such an incorrect proof.
Both impressive and terrifying. But as always, the methodology is buried: how many open problems were tried until they found a success?
If they tried this on 1000 problems and this is the one that succeeded, it still means that there are 999 open problems that an LLM cannot one-shot. It seems likely that this would remain the situation until the next model.
If this is the first one they tried, maybe we’re totally hosed.
The conclusions are so different in these cases that it is impossible to know what to think. Though it is reasonable, I think, to assume that a company is willing to push the maximally misleading narrative —- especially a company known for questionable ethical direction at the top, and one that is still circling an IPO, and one that is in the tech industry, where conjuring an illusion of growth and progress is sufficient for success.
> But as always, the methodology is buried: how many open problems were tried until they found a success?
Not only that, but they have like 500 world-leading experts in mathematics and IMO alumni, so how do we know one of the agents wasn't hardcoded to return a proof that the mathematicians had found?
I'm a mathematician/graph theorist, and I've tried ChatGPT 5.3, 5.4, 5.5, and now 5.6 on a bunch of simple-ish open problems, and I've never gotten a solution.
I’ve had a similar experience in physics. Excellent domain knowledge and semantic search, but the intellectual sparkle and reasoning just isn’t there and it still often throws out a lot of wrong ideas. It is very useful for coding.
But there is a discrepancy between (the implication behind) these reports and how I subjectively feel talking to LLMs. Granted, I don’t have access to whatever cutting edge model is out there for as many credits, but I also don’t feel like I’m talking to an IMO silver medallist.
I like how the proof is so concise. I made progress on some unsolved combinatorics problems but the proof was 45 pages long to extend the frontier by one step.
I did some math research in high school where the proof boiled down to dozens of cases of ugly polynomial inequalities. I can't find the PDF now, but the final paper was something like 70 pages, and several of those were full-page polynomial expressions expanded out. The actual prose was probably 5 pages or so.
It was categorically the least elegant proof of anything I've ever seen.
I'm incredibly grateful to for the opportunity to have done the research and gotten my feet wet early on, but boy do I cringe when I look back at that paper.
Reading the prompt is very interesting. I always wonder how they make these long-running prompts and I guess they literally just tell it to "keep going".
After working with LLMs day-in, day-out an SWE for months, I feel like this could be greatly improved with something like a state machine of progress and proper orchestration. Instead of spinning up a ton of subagents to follow different paths, whip up some Markdown (or LaTex or whatever math-equivalent) to store summaries of attempted paths, and have the agent augment those docs. Leave a paper trail of what has been tried. Iterate on that paper trail and repeatedly examine it for untried alternatives.
LLMs can construct, navigate and summarize exceptionally well. Why is anyone trying to make them "hold the whole thing in your head"? I may be completely off the mark here since I have no math background, but my intuition for how LLMs are able to build on understanding through an external context store makes me feel like this isn't much different than someone trying to one shot a 3D game with Fable Max for $10,000 when they could get the same, or better, result with more human intention.
> I always wonder how they make these long-running prompts and I guess they literally just tell it to "keep going".
Many harnesses support a /goal as well. When the agent thinks it's done, another LLM compares its results to the goal, and if not, tells it to keep going. It's quite easy to have agents working on something for hours this way.
What you're describing is similar to how the copilot harness in vs code tracks state and previous work. These systems are being implemented, bit by bit.
Especially with GPT (5.5), I've been having a lot of issues with it just repeatedly stalling out. I had to build a quota monitoring skill so that it'd keep plowing forward until either the task was finished (in some way) or the quota budget was exhausted.
I also had issues with the compaction. Codex seems to compact... weirdly, resulting in the agent becoming a newborn after each compaction event. Telling it to use a notes file is basically essential and self-evident.
Now that I mention, I should probably refine this skill to monitor the context window fill as well, to work around this.
I am torn by these announcements. On the one hand there is the infinite potential on what we can disover, when AI prompts are solving outstanding problems. On the other, something is lost in an aesthetic sense when it wasnt a man working through this or with a novel insight. If an AI prompt runs on a data center for two weeks and then prints out p=np, it feels a little empty.
"Keyboards are soulless. Handwriting is personal – as unique as fingerprints." - Joyce Carol Oates on typewriters
"This discovery of yours will create forgetfulness in the learners' souls, because they will not use their memories; they will trust to the external written characters and not remember of themselves. The specific which you have discovered is an aid not to memory, but to reminiscence, and you give your disciples not truth, but only the semblance of truth." - Socrates on writing
It's a good outcome as long as the proof is valid and ubderstandable to humans and leads to the discovery of further knowledge. There has been decades of search in Theorem Proving; this is just the next step.
I resonate with that feeling, but on the other hand the humans reading the output will receive a pretty big boost in inspiration; new answers usually prompt new questions.
[deleted - the paragraph immediately following the proof of Lemma 2.1 is crucial and I found it hard to read correctly on my phone with the cramped typography. Having reread it I think the proof is correct.]
It's just a way of breaking down the full proof into pieces.
Lemma 2.1 says 'if this assignment exists then X'
Then later in the proof you say 'here is such an assignment, so, applying lemma 2.1, therefore X'
You don't need to assume the existence of the assignment, you prove that if the assignment exists then something else follows, and then later if you can find that assignment then you get the result of lemma 2.1.
Just dropping in to say it's nice to see somebody actually try to work through the proof, and it gives one confidence that the proof at least isn't complete nonsense (which is helpful given the few details provided about the process behind it).
With the Erdős proof, OpenAI added perspectives from working mathematicians that gave some context -- hope something like that appears for this one eventually.
I was not a fan of the writing style of the proof. There seem to be some irrelevant details: Is the mention of 8-flow at all relevant? I, at least, found the definition of L on the first line of the proof of Lemma 2.2 to be needlessly inscrutable, and my thesis advisor would have likely stopped reading there and told me to fix it.
Maybe someone should ask the model to make a more clearly written and thus easy to verify proof :)
I was confused at first when you asked if the 8-flow is relevant, when like, the 8-flow is a key input that the cycle double cover is built out of. Then I realized, oh, I guess technically they're not using the 8-flow, they're using the Z_2^3-flow. But like. The existence of an 8-flow and the existence of a Z_2^3-flow are equivalent, and I gather most graph theorists are going to talk about it in terms of the existence of an 8-flow, so noting that having a Z_2^3-flow is equivalent to having an 8-flow helps the reader to put this information in context.
I'm not sure why you find this proof so hard to read. I found it mostly quite readable (and the definition of L is straightforward? I wouldn't have written it quite that way but it's hardly inscrutable), although I feel like some parts are maybe lacking some exposition to explain the reason for certain things -- it doesn't feel written "in order". I also don't like that it's not cleanly separated into theorems and proofs -- some of the proof occurs in parts that aren't set off, for instance, and there isn't even a proper main theorem statement! But overall I was able to get through it without a lot of trouble and I'm not even a graph theorist...
My issues with the definition of L are mostly about the order in which things are written.
L(t, epsilon)_e breaks down the range of L onto its component values indexed by edge, but this only really makes sense when you know that t and epsilon are. They are sort of defined in the middle of a sentence in the proof of 2.1, which IMO is asking a lot of the reader, and this sort of sloppiness is a way that errors can hide in a proof. (Not that I see an error here. But a formalization in Lean or whatever would not get away with this.)
And, in the same definition of L, for some reason the e=uv part comes at the end only after u and v are used.
What would be wrong with stating, in the definition, what sorts of objects t and epsilon are and with omitting e entirely in favor of just calling the edge uv everywhere?
are the references real? how do you think it got access to those papers? were they somehow already in the training data, or a result of web searches, Google scholar, etc?
None of them include a web URL but in text some are super specific ("[3, Sections 2.1 and 3.1]" and "[8, p. 367]").
The references go back to 1954 (Chronologically sorted: 1954, 1973, 1975, 1976, 1978, 1979, 1981, 1985, 1987 and 1994.)
Since reference 10 is included as "personal correspondence" maybe the reference itself was copied from one of Tutte's other papers? Or how did it get that reference?
If it were a human (going off of memory as it has been a while), they would probably be using mathscinet and their university library to obtain copies of these papers online. Many old papers are digitized and available by these means. I’m sure the AI companies have it all easily accessible and/or the entirety of mathscinet is in the training data. The “personal correspondence” is possibly lifting from another paper or journal but yeah that is a bit odd that they wouldn’t source where they lifted that from directly.
I can’t say if the citations are accurate because I didn’t check.
Sloppy scholarship. On the other hand, it's simply a credit attribution of posing the problem, so it's not material in evaluating the results. I observe that the majority of references I can find that attribute this to Tutte are very indirect - i.e., citing sources that themselves claim Tutte was one of the people who formulated it - so it would take someone with a little more time on their hands (or perhaps an LLM) to track down the original...
No, that's not a problem at all. It just the notation that's a bit weird.
For example, if e is the a-edge (first edge) from the u side and v is the b-edge (second edge) from the v side then g_{u,e} = 0, g_{v,e} = a so d_e = 0 + f(x2) where f(x2) is the flow (from Kilpatrick and Jaeger's NZ8F) on the first edge next to v.
I checked the whole thing with some surface reformulations on my side and it looks right to me.
That's a much shorter and more elegant proof than I was expecting, especially after reading some of the earlier Erdos proofs. GPT 5.6 Sol is the real deal.
I just had Sol Ultra read the proof and create a graph of it using Concludia (my side project) so you can explore it visually/graphically. I certainly don't understand it though so I have no idea if it's helpful. :)
Is there anyone more knowledgeable than me about proof checking software who could tell me how off the mark I am here?
Assuming you have decent proof checking software, is it possible that this solution was achieved by throwing GPT at the problem a couple hundred thousand times until it passed the proof checker?
As someone who's used proof checkers a fair amount, if you don't have some high level idea about the proof, it's an open problem, and the hard part isn't some extremely tedious finite case analysis, it's extremely unlikely you'll get anywhere by trying to mechanize by throwing stuff against the wall to get it to typecheck. When people talk about mathematics being a closed formal system as though this trivializes any creative component, what they're omitting is that in type theory like that used by Lean or Rocq, there are two kinds of terms (match statements proving dependent elimination and fixpoints that provide proof by induction) where there's no real way to infer the type from the term. i.e., there are cases where you have to get creative and try to prove something more general than what you actually care about in order to get the proof about the original case to go through. What does "more general" mean? It could mean anything... that's the problem. That's why it's usually advantageous to reformulate the problem in terms of a different abstraction and build on top of existing results, knowing a lot about the literature and the way these kinds of problems tend to be attacked, rather than just chuck random terms over to a proof assistant and hope for the best.
Well the key thing here is I’m not saying the LLM has no idea what it’s doing. But LLMs are prone to hallucinations which can really impact a string of interdependent logic like a proof. So I’m assuming it would respond with something that’s not complete nonsense to this proof most of the time. Where I’m skeptical is if this was a true one shot, or if they had to iterate and try multiple different prompts, or even the same prompt over and over again to reach a working solution.
So I’m just asking if the proof checking software is capable of evaluating this proof. Because if it is, that makes the brute force approach a lot more feasible as you reduce human review overhead significantly.
If it is, that would imply you could run the prompt through the LLM as many times as you want until you “strike gold” so to speak.
I absolutely think that with the rise of LLM generated theorems we need mechanization more than ever, yeah. But I felt that was already pretty important for human proofs, too, and people are just more amenable to the idea now that it doesn't take such heroic effort to formalize things.
As far as whether something like Lean could evaluate this proof: sure, if it were mechanized rigorously. But the amount of work that takes to do varies with both subject and complexity of result. In this case, from what other people are saying, the infrastructure for doing graph theory proofs like this isn't as built up as it is for some other areas of mathematics, so it might take a while.
I'm honestly not familiar enough with how well-developed graph theory is in Lean to be able to say. The paper is mostly using pretty old results, so it's mostly a matter of whether that stuff has already been formalized or not. Like anything else in software (and Lean proofs are very much software) a lot of it's about infrastructure. It wasn't so long ago that no area of mathematics outside of type theory and formal verification was really built up enough to do "serious" math -- that's changed a lot within the last few years.
What I'm more saying is that we're a ways away from being able to straightforwardly go from an LLM having a paper proof to having that proof formalized in Lean in the general case. Not so much because it's hard for LLMs, more just because it's hard in general unless all that background work has already been done. As more and more of foundational mathematics gets mechanized, it will be easier and easier to check your work in Lean while you work on the proof. For example, AFAIK unit distance has already been mechanized (though the quality of the mechanization effort sounds not great, it still greatly increases our assurance in the proof's correctness).
"But LLMs are prone to hallucinations which can really impact a string of interdependent logic like a proof. So I’m assuming it would respond with something that’s not complete nonsense to this proof most of the time."
Unfortunately in my experience that's not really the case. For me, very often GPT 5.5 (which was a good deal better than Opus at this kind of task) would just get stuck for long periods when working in a logic like Iris. It wouldn't necessarily outright prove nonsense, but it would vastly overclaim what it had proved and failed to get anywhere without a lot of hinting. 5.6 is hopefully a lot better about this.
As someone who was a research assistant in this field one summer back in college, I spent the day trying to check the proof, or at least the obvious places a mistake would be. It's surprisingly readable, so I guess we'll find out soon.
Lemma 2.2 specifically "feels" new to me. You can get part of the way by duct-taping several papers together (playing along at home: I found Tutte 1954, Bermond–Jackson–Jaeger 1983, Máčajová–Škoviera 2005, Zaslavsky 1982. interestingly, only Tutte appears in the works cited). But it's surprising you'd think to pick those, and surprising it works, because you still need a genuinely novel parity argument at the end. Those steps individually are all pretty simple, knowing to chain that chain together, isn't.
The guess-against the checker paradigm is real (ie AlphaProof), and something like that was probably involved here. But this area of graph theory isn't in mathlib, you need to write the proof checker first, and then you need to know what kind of proof checker you need to write (or just do a brute force search for new proof checkers). Probably how you got this result is have a recursive tree of agents until you divide into small enough subproblems.
At a certain point you need a philosopher to figure out what that "means", ie if you have a big enough tree of small enough subproblems, some of the "magic" so to speak moves out of the proof checkers and into the way the tree got structured.
On the last Dwarkesh podcast with 3blue1brown, one of them mentioned that frontier models are now able to work through a whole proof in natural language, just like a human mathematician would. But when they first solved IMO problems in 2024, they relied more on Lean to catch hallucinations.
> GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture
Very misleading article title.
Title should be "Un-named humans produce unverified proof of CDC Conjecture using GPT-5.6" ... but I expect only advertising copy when it comes from the AI industry.
It's been amusing to watch the points bounce up and down on my comment.
I guess equally half the readers agree with my sentiment, and half down-vote, being upset by my attitude to the AI industry :)
PS. I'm quietly waiting for the bubble to pop - the main interest being will it pop with a bang and cause grief to many, or will it just go with a long drawn-out fart that can be ignored by most.
This is not a remark about AI, but there's something funny about mathematics in that every novel result is broadly perceived as a big deal.
We attach basically zero value to writing a new program that hasn't existed before, or a piece of text that hasn't existed before. It's boring, or even a net negative, unless you can show that the result benefits the world in some way. We'd find it weird if OpenAI put out a release saying that an LLM authored an interesting blog post.
For mathematics, I think it's really a matter of two things. First, the generation of proof was so severely resource-constrained on the human end that they could actually afford to celebrate every contribution - akin to how software engineering would look like if you had just 200 active SWEs in the entire world. But compounding that, mathematics is basically the only scientific discipline that rejected any notion of utility. It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
> rejected any notion of utility. It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
I disagree. Mathematicians care about the utility of a result. It is just that they regard mathematical understanding as a valid type of utility, and that can be arbitrarily far removed from practical utility. But a proof that doesn't help anyone understand anything interesting is not valued. I could go out and define some pointless construction and create proofs about it immediately. It would only matter if I connect it to some other subject of interest within math.
I would argue that mathematical understanding is valuable for extrinsic reasons, but it is true that by the time you're a math grad student, you're usually willing to pursue it for no external purpose.
It seems in mathematics that the utility of a problem is directly correlated with how difficult it is to solve, for some odd reason. If I defined some pointless construction and it turned out to be very difficult to prove, it would automatically over time become considered a "high utility" mathematics problem (again, for some odd reason).
Mathematics is largely just smart people working on pointless puzzles, and only by coincidence do these puzzles turn out to have practical applications (it cannot be predicted). Or I guess all the obviously practical problems in mathematics have already been solved -- we're now in a world where math is rarely the limiting factor for human progress (like it was, say, pre-calculus; was FFT the last significant unblock from math?).
It's such a waste of the best human minds. Or maybe the best human minds are actually doing something else, maybe we only notice the handful of Terence Taos, not the hundreds of people of equal brilliance who realized pure math is pointless and decided to pursue physics, rocketry, or quantitative finance.
> If I defined some pointless construction and it turned out to be very difficult to prove, it would absolutely and automatically over time be considered a "high utility" problem (again, for some odd reason).
Yes and no.
No: There are lots of very hard open problems which are judged to be of little value by mathematicians and hence garner little attention.
Yes: If a conjecture resists proof for a long time, this can indicate that we still have a substantial gap in our understanding. We project utility into an eventual closure of this gap, not into the statement of the concrete conjecture at hand. The gain in understanding is what we actually work for. It just turns out that chasing specific results, even if they are mostly dead ends on their own, is useful for orientation.
The (by now solved) problem by Fermat (for all integers a ≥ 1, b ≥ 1, c ≥ 1, n ≥ 3, the equation aⁿ + bⁿ = cⁿ does not hold) and the (still open) Collatz conjecture are perhaps good illustrations of this situation.
Your comment is somewhat emotionally charged, but I choose to respond to the overall point as a mathematician. I think it could be true that utility is correlated with difficulty but it is certainly not defined by it.
In pure mathematics, we reason about a world of abstract objects which are considered interesting ab initio. It may be because they arise directly or often from extremely basic operations, they are connected to many other interesting objects, or that they present special and surprising properties. The importance is basically, there is some surprising, interesting, phenomena which occurs in our world which we don't understand and which we seek to understand. Like science but in the non-physical world.
I think if you create a simple to describe system/construction with a property which is extremely difficult to prove. You are creating an object in our world which is basic but have properties which we don't understand (because we can't prove this property). So indeed I believe it would be an interesting thing to study and be of value. I don't see any problems/issues with this. I don't think the only valuable pursuit of humans is to improve the welfare of other humans. I think understanding the world is also valuable.
Most fields, in the aggregate, produce a lot of pointless work, but if you judge mathematics by its best examples, as judged by the field itself, and also by the outside intellectual community, it is a coherent body of work (& brilliantly creative). It is not pointless puzzles at all. William Thurston's geometrization theorem, Klein's erlangen program, Witten's work in physics-inspired mathematics, Langlands program, the Grothendieck school of Algebraic Geometry are deep and abiding intellectual achievements of true understanding. If you don't understand the meaning behind this work, it speaks to your ignorance, not to their significance. The "obvious practical problems" are not solved. Fluid Dynamics is wide open. Non-perturbative quantum theories are wide open. Heck, there are open mathematical problems in General Relativity. Dynamical systems are very poorly understood. Go read a book or something.
There was no useful math after 1964? What? Or do you not count the entire field of computer science as math (arguably FFT belongs to computer science too)?
>mathematics is basically the only scientific discipline that rejected any notion of utility
I think this might depend on the department, but I was at a pure math department last year, and struggling with my Linear Algebra textbook (written by the professor, incidentally, who was not a great communicator).
I consulted the machines, and learned, to my great delight, that linear algebra is used in like 20 different fields in the real world. It's "perhaps the most applied branch of mathematics in existence".
I complained in the group chat, that our didactic materials, specifically tasked with providing motivation and concrete examples, did not contain a single application, of this most richly applied field.
I was promptly pilloried, and shunned.
(Apparently that particular department was the wrong one, to ask a question like that!)
I’m a physicist, so I’m biased, but my experience of pure maths was about the same. We had to do it, but at no point was any utility actually demonstrated - that was left to the physics professors. It was all just “look at this thing I can do with these symbols” without any actual tangible relationship to anything.
Then again, I remember how we were taught calculus at high school - we were taught how to mechanistically integrate and derive everything under the sun. At no point did anyone think to explain that we were measuring the areas under curves, or their rates of change - it was all just “memorise this operation”. Again it was left to the physics teachers to explain why this was useful, and what we were actually doing.
Poor teaching, if you ask me, and it more often than not left me retrospectively wondering if said mathematicians had actually understood any of what they did, or if they just had little blind symbol manipulation Turing machines in their heads.
I remember squinting at the definitions in my calculus textbook for a full 10 minutes before realizing... oh my God, if this had been a 5 second animation, I would have understood it instantly.
I remember being rather upset! "If it's so obvious and intuitive, why didn't they just say so?"
I want to say, "well, unfortunately you cannot put an animation in a textbook." But that's actually false!
Even as a child I made flip book animations. And there was plenty of room here in the margins for several of those :)
Teaching only the practical side risks not teaching the subject with the appropriate theoretical depth and the ability to generalize it to other applications. Courses for purely applied fields utilize calculus to solve the current problem and then move on without teaching the finer points. Basing a calculus course on physics alone might be preferable in high school, but would be of disservice to students in university.
>At no point did anyone think to explain that we were measuring the areas under curves, or their rates of change
In my experience you get taught the definition of a derivative of a function at a point is equal to the instantaneous rate of change and that integrals are defined as a Reimann Sum, the sum of the area under the curve. Everything in the class comes from building on top of those definitions.
That you think this way (and if like me, it makes you excited!) I think it's because it has clicked for you.
For many that light bulb above their head doesn't flash on, hence they get to dislike the subject or forget it after they are done with their studies. I was lucky enough to appreciate math that much to redo it in my free time after high-school and make it click for me.
No, my calculus class in HS very literally started with finding the area under a curve “manually” and introduced integration as a generalization of that. I’m not surprised to hear that calculus is sometimes taught very poorly, but it’s not universal.
The title is a slight misnomer in my opinion. The author did make heavy use of spaced repetition of course, but deemed it neither necessary nor sufficient for the result he described.
The actual active ingredient is curiosity to the degree of obsession. Actually wanting to understand what's going on.
You can do that with pure math just as much as with applied.
But it may be harder for many people for such a desire to arise if there is no obvious connection to real-world matters. (I certainly had such thoughts, sometimes! What is this for? What's the point?)
> I complained in the group chat, that our didactic materials, specifically tasked with providing motivation and concrete examples, did not contain a single application, of this most richly applied field.
> I was promptly pilloried, and shunned.
Heh. In my day I may have participated in the pillorying.
I do think that there is value/merit in professors mentioning real world applications, where they exist.
What they're sensitive about are the theorems where there aren't real world applications. They don't want to (and shouldn't) justify them.
So even when there are real world applications, the posture is "Who knows if someone is making good use of this in the world somewhere? I don't care. It's not why we learn or teach this!"
Knowledge for its own sake is great, but it's worth noting that many "useless" fields of mathematics turned out to be very practical in the long run.
Number theory was long thought to have no practical application, but now it's the backbone of cryptography. Boolean algebra was developed in the 19th century (George Boole died in 1864), decades before it was used to build computers.
Those "useless" theorems being proved today may turn out to unlock a world-changing technology centuries from now. When the breakthrough comes we'll be grateful for the people who laid the foundations.
For a lot of math departments, that is exactly why they teach this. Education is rooted in application. We have entire careers that depend on certain aspects of mathematics, so most companies gatekeep that career by a degree. The degree requires the class. The student taking the class may not even be old enough to drink alcohol yet, and they can't possibly be expected to know of all the applications. Knowing and not telling them is doing them a disservice.
> For a lot of math departments, that is exactly why they teach this.
Depends on the course. That's why some departments have separate calculus courses for math majors - because otherwise the whole class will be full of non-math majors (engineers, etc) and focusing on their needs does a disservice to the students in their own department.
> The degree requires the class. The student taking the class may not even be old enough to drink alcohol yet, and they can't possibly be expected to know of all the applications.
If I'm a CS major, and the degree is requiring a class outside of the CS department, you shouldn't expect the professor of the class to know why the CS department is requiring it. It's on the CS department and its faculty to explain it.
The ultimate goal of university education is to raise researchers, who are the people that investigate the knowledge frontier of their field and then advancing it. To do that they have to understand a large part of the existing field so they can communicate with their peers, avoid investigating things that have already been throroughly explored, and draw useful connections to other fields.
Even in more applied fields it can take decades before advances become practically relevant. Restricting teaching to topics that have immediate practical relevance would therefore do students a huge disservice and prevent them from approaching the knowledge frontier of the field.
CS is special in that it is about the science, and not the application. They'll teach you mostly theory. That's why some universities/countries have a separate degree called "SW Engineering".
Other engineering departments are not as fussy about the distinction.
I think for many people (myself included) understanding mathematics is rooted in application because it helps bridge the divide between intuition and rote memorization. Without the application, IMO instructors are doing a disservice to their students and pedagogy of mathematics itself. They’re intentionally ignoring a significant fraction of the class, unless they’re teaching some esoteric grad level pure math.
Yeah this was my position. I don't mean "Sally has six apples" necessarily, but my brain needs some concrete handles to grab onto so it can actually manipulate this stuff intuitively.
See also: Using spaced repetition to see through a piece of mathematics
Where the author describes his mind eventually turning the mathematical objects (symbols) into some kind of mental objects he was able to actually manipulate "directly". As a result of this facility, his mind spontaneously produced many new insights into the matter.
That level of fluency obviously requires a great deal of work, but in my experience it can be approximated and accelerated with analogies. (e.g. see Feynman's teaching.)
I love teaching kids and young adults calculus by socratic method. They get so mad when they figure out you were teaching them math, but they often admit it was pretty fun. Only had the chance to teach like that a few times but it's dynamite when it happens.
I did this when I taught my third grader calculus on the train, when she asked a question about the train accelerating faster sometimes than other times. She loved it, but I was just taking advantage of children's natural curiosity.
Do you have some examples that the adult could instigate, rather than waiting for the child to express curiosity?
I've used filling a tank, balloon, or bucket (rate of flow, can be subdivided to teach limits, and use weird shapes for teaching area under curve and interpolation en route to integrals), or the classic throwing a ball back and forth and trying to describe the shape, the distance it flies, peak speed vs peak height, figuring out how hard you are "actually" throwing instantaneously. Honestly as soon as you start thinking about bulk substances moving around (gravel piles! fuel tanks!) it's easier to find examples than you'd ever reckon. Rate of change is everywhere.
Seems like I start by asking "how do we know how much this tank holds?", or "how fast does this line go up on the side of the tank?" and curiosity goes from there usually.
I thought linear algebra was pretty much the poster child of applied mathematics - the entire field was invented to represent computations in a regularized form to feed into computers. Well not really, but much like Boolean algebra or the Fourier Transform, it was pretty much a curiosity until computers came along.
Many important advances in linear algebra happened in WWI to solve optimization problems for logistical and industrial planning. A lot of these applications boil down to high-dimensional systems of linear equations, which back then were solved by hand. Efficient algorithms translate to reduced labor costs.
despite being theoretical i would have greatly benefitted in learning linear algebra if i had seen even one or two not-obvious applications, like galois fields for reid solomon erasure coding.
Even when this really isn't the case, the math is preferably reduced to a linear problem whenever possible since dealing with the original complexity is usually so much more painful.
As a friend of mine who also happens to be a math professor once said: mathematicians are like sculptors who marvel about the beauty of their creation, and are kind of disgusted when a physicist comes nearby and says “that's a cool hammer you got there, may I borrow it?”.
Typical pure-math linear algebra course has to cover so much material that there's really no time for applications! That's why applied math is typically separate track.
Biologists celebrate the discovery of new species of fruit fly hidden deep in the Amazon rainforest. Astronomers celebrate the discovery of new giant rocks located zillions of light years away. Neither of these things is immediately “useful” to the world, although they may turn out to be enormously beneficial in ways we can’t immediately predict. To me, these fields also feel central to the human experience—discovering new types of life, or learning more about our place in the universe. I don’t think a mathematical proof is any different.
> This is not a remark about AI, but there's something funny about mathematics in that every novel result is broadly perceived as a big deal.
This isn't true using the level of originality you're implying with your software examples.
Technically speaking, many novel mathematics proofs are written all the time (quite a few textbook exercises are actually technically novel problems that have never been posed before they were written in a textbook!) that get absolutely no fanfare. Overwhelmingly though they are not very original or difficult and really just required a fairly routine combination of different pre-existing techniques, even if technically speaking that combination didn't exist before. Those textbook problems are hence easy and therefore not given much public attention even if they are technically novel problems.
Indeed over the course of developing a new mathematical result, many many novel results are glossed over to the extent that even their proofs are left out ("as an exercise for the reader") because they are fairly trivial.
This is true for the overwhelming majority of new software as well. A new CRUD program may, technically speaking, be novel, but it's almost certainly just a routine combination of different pre-existing things.
Mathematics open problems that are actually named are generally problems that have resisted the low hanging fruit of the most obvious combinations of pre-existing problems. When those are solved they are a big deal precisely because they usually require some novelty!
Similarly in software, if someone were to create a new kind of database that solves a variety of new classes of problems that current databases fail to solve that would be a big deal! Truly novel software is also perceived as a big deal. Software that is, technically speaking new, but doesn't actually stray far from a fairly obvious remix of pre-existing techniques, isn't really celebrated.
In both software and mathematics, the intuitive benchmark is if other practitioners in the field look at the result and would say "Wow! How did you do that?" Professional software developers generally don't look at, e.g. a new blogging platform, and boggle at "Wow! How did they make that?!!"
I'm not a mathematician, but I don't think that's true..? It's just that some problems are considered "hard" or known to have been "open" for a long time or that involve some clever/pioneering new technique. There's tons of math papers out there that are in some technical sense a novel contribution but in practice just languish without much attention except maybe from like two other people working in the same subfield.
This feels mistaken; we develop abstract objects i.e. graphs based on real-world utility or whatever. As we try to improve our understanding of graphs, we value proofs that help us do so, or help other fields of mathematics. We assign 0 value to random proofs about stuff no one cares about... This conjecture had value, simply because some people found it interesting. It is not really different from music, in a sense.
> It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
No, the value is that Erdos's name is attached to it.
Lots of mathematicians prove things they don't publish, or their manuscripts get rejected - not because of a flaw in the proof but because no one cares about the theorem they proved.
And I'm sure it'll be the case with LLM models performing proofs. It'll be notable only when the theorem is a known one that people have had difficulty proving.
It’s far from a perfect analogy but I would imagine that people were pretty hyped about the novelty of the first legitimately useful compiled programs where they didn’t have to allocate their own registers. I wonder how long it took for that novelty to wear off?
Or in other words I’d argue novelty is contextual and that these kinds of discoveries’ novelty will eventually wear off too but for right now it’s pretty cool that the “math discovery compiler” works well enough to do this (again imperfect analogy).
Math is something humans invented and is a model, nothing else. There is no logic per se, but a model that works quite well for us.
I studied Math and CS as a very highly gifted and quickly found out, there is no beauty of Mathematical Logic, only humans approval of what they deem most accurate.
A good example is set theory. Cantor was not openly welcomed after he introduced his "theory" to others. In fact, he was received quite some pushback and hostility - this doesn't sound like someone received love the mathematical logic's way.
In fact, the story of Cantor is really a tragic one. He left math for quite some time, due to the pushback.
Only later humans accepted his theory and found it useful. Well, well, what is Mathematical Logic and what not is after all just broad consensus by humans.
And if you go deeper, you will hear more of these stories. Math is anything else but logic. Proofs are religious things, often so complicated, they are simply accepted as "approved by a committee". Many profs cannot really explain simple proofs, they refer to the textbook.
This doesn't sound like romance nor easily reproducible logic.
Consensus may give a hint to what is or isn't reality. But consensus—even expert consensus—does not determine reality. Experts can be wrong. Most of the experts, even, can be wrong simultaneously.
Philosophy is the exercise of testing ideas for oneself in the laboratory of one's own mind.
When I test the idea that math is discovered in my own mind, from my own perspective, with my own experience and education brought to bear, I find it unconvincing.
When you test the same idea in the laboratory of your mind, with your experience and your education applied, and get a different result, that is interesting. Your result is relevant information to me. If nothing else, it's a good prompt/trigger for me to revisit my earlier conclusion and see if it still holds.
But your disagreement—or indeed, the disagreement of a majority of trained mathematicians—does not constitute an automatic reason for me to conclusively determine that you/they are right and I am wrong.
I still have my own examination of the concept, with my own supporting and detracting arguments. And the result of my examination continues to be that math being invented is the significantly more persuasive view.
> We attach basically zero value to writing a new program
What does it mean "new"? And, was it a difficult or trivial accomplishment?
A solution to a well known open math problem is both new and non-trivial- you know that many, very smart, very well trained human experts have dedicated time to the problem and haven't been able to solve it, despite good incentives.
There is a tension between applied and theoretical mathematics, and it's as old as the whole science itself. Mathematics arose to solve practical problems (land surveying and division, as well as trade) and recognizing the underlying principles make it possible to abstract that knowledge. That might lead to centuries of ivory tower activity and what could be regarded as a purely artistic pursuit until somebody figures out how to apply a theory to a new practical problem. Or relations to another theory are discovered, and suddenly there is a new approach to previously intractable questions. A good example is be number theory, which is the foundation of modern cryptography.
> there's something funny about mathematics in that every novel result is broadly perceived as a big deal.
Is this true? Or is it just that mathematics is an isolated enough field that only the results that are a big deal get broadcast widely to the public.
I know little of the inner workings of the field of mathematics, but my naive assumption would be that there's probably lots of novel but boring results being discovered/proven all the time and we don't hear about them because no-one outside of the person doing the work and a handful of their colleagues is really that interested in it. Likely a lot aren't published in any way, because they're just stepping stones towards the goal of the actual area/paper/whatever being worked on.
The reason novelty matters for mathematics is that they strictly deduplicate all claims. If someone claim they proved something that we already knew was solved, than that wouldn't be considered novelty. Novelty and deduplication is the combo here. This is not true for blog posts.
The difference is discovering or proving a universal truth that will go into the corpus of human knowledge forever versus some app to shuttle money around or help people count how long they’re sleeping. It has gravitas unlike some nifty super performant text editor.
> We attach basically zero value to writing a new program that hasn't existed before
We don't? People write new programs that go on to be successful software companies that make millions of dollars! Basic CRUD apps make money for their creators in their niche! There's so much money in software that it's taking over the world. The market is different, you're not getting worldwide household recognition for every little fart or sneeze of programming you output, but how can you say that we attach zero value to new programs when the history of computers is insanely valuable companies making new software and selling it. Windows, Oracle, mongoDB, etc.
> It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture..
I'm not sure about this, TBH I ask myself this quite frequently. In a world where machines are routinely solving very high end math problems every day, producing more proofs than humans would ever really be able to absorb or fully understand.... would that be a good thing? Would that in itself be valueable? It feels like that is a probable future, but I'm not sure that would actually be something we want. I think there's probably more than "value is that it's solved"
Isn't it immediately obvious that solving something that humans have been unable to do for decades or more is the most tangible proof of ASI, or at the very least pretty good AGI?
There’s only so many people with the necessary skills to solve this. And you need these humans to choose to spend their time solving this, and not something else.
>There’s only so many people with the necessary skills to solve this. And you need these humans to choose to spend their time solving this, and not something else.
Sure, but that doesn't mean a lot of very skilled people hadn't attempted and failed to solve this.
A lot of mathematics often takes 100+ years to find a practical use because we have developed it so much that we have use all the easy maths. Things like CS or SWE are so new that you can still find stuff today that can be used tomorrow. Things like computation and cryptography was all discovered like 100 years before we had a practical use for it. Its an example of late stage scientific discipline. Things like physics, chemistry and biology will get here as well eventually.
It's newsworthy because it's a milestone. It was something no human was able to do (despite trying very hard), but a machine did. Humans have written lots of interesting blog posts.
The idea that mathematics has rejected any notion of utility is absurd. It's not like topics get picked at random. Conjectures like this are interesting because they are a test of our understanding. The problem sounds easy, but apparently was quite hard.
there is no "software" that a lot of people want, yet nobody managed to create yet because they failed too due to it was being hard to implement (excluding AGI/ASI which is not really software)
As a person who has a number of relatively niche hobbies, I assure you that this is not true. There's a ton of simple things that can be build and will make an immediate difference in the lives of thousands. Watch the workflow any musician, videographer, machinist, etc - they're full of small, weird inefficiencies that AI hasn't really solved for them.
It's just that you can't build a billion-dollar company around it. No one could go to a VC and say "we're going to be the Uber of focus stacking and dust removal for microscopy" or "we're the Uber of aligning the beats in two audio tracks".
> there is no "software" that a lot of people want, yet nobody managed to create yet because they failed too due to it was being hard to implement (excluding AGI/ASI which is not really software)
What!? I can think of about a billion examples... but for one, I'm still waiting for a good enough CFD/FEM coupled system to model paraglider dynamics across collapse/recovery. And I expect to be waiting quite a while.
5 minutes of wikipedia search would give you plenty examples of complicated software engineering problems that would have a big impact on everyone's life.
In math, the utility lies in the proof itself. A novel proof of a hard problem usually comes with new insights and abstractions that help solve even more mathematical problems.
To go with your analogy, mathematicians care more about the source code of the program than about the result of the program. But I'm afraid that we will see things change with the increase of vibecoded proof slop. A black box proof is not as useful, even if it is correct.
Mathematics is what everything else is built upon. I'm no mathematician but a very good friend of mine is: teacher at a big uni, researcher. Pure math.
His entire life he's had --and still has-- to deal with comments like the one you just made, implying that the only value is solving pointless conjecture (if it wasn't pointless, according to your logic, then the value wouldn't be that it is solved).
"every novel result is broadly perceived as a big deal" is not at all true. AI companies hype any novel result as proof that AI is good for mathematics, but professional mathematicians write tens of thousands of papers every year, and for 99.99% of them, nobody cares or writes it up. Mathematicians certainly don't go around saying each and every novel proof in their papers are a big deal. Do you have any evidence supporting your statement that it is "broadly perceived" (by whom?) as a big deal?
Sorry but I completely disagree with your statement that "every novel result is broadly perceived as a big deal". Most results certainly are not consider this way (even though the average result has difficulties that are much higher than novel computer program you may have in mind -- no offense)
I mean, OpenAI delayed the public release of GPT-2 back in 2019 because it seemed capable of authoring interesting blog posts (that also happened to be untrue). It was a pretty big deal the first time Transformer models were capable of generating that kind of output--no one found it weird. We've just grown to take it for granted that large Transformer models are this capable.
The same cycle is happening now for a harder frontier. And proofs represent a pretty good benchmark for model capabilities, so a new model proving a result that a previous model didn't is generally notable in the same way that a model scoring higher on a benchmark is.
I'm sure we'll take it for granted in the not-too-distant future.
We generally do give a lot of credit to programs that do something novel. The first gets a lot of credit. But if its just another CRUD app, nobody cares.
Its the same with proofs. First time someone proves something gets a lot of credit. The second proof for the same theorem gets a lot less buzz.
But even then, math proofs mostly get buzz when its something famous or at least important. Proving a random lemma usually doesn't get much buzz.
So I suppose the value is that something like this gets used as a primitive to solve something that actually has impact. Ah, mathematics, never change!
There's really no good proof system mature enough to do advanced graph theory. The leading library in Lean is Graphlib, and it's really not ready for research level theorems.
Yeah it's a very very short proof that uses no mathematics developed within the last 30 years. Which doesn't necessarily make it wrong, but in the absence of mechanization in Lean or proper peer review I think this it is premature to post this. Notably the unit distance proof did not fall into this category.
Let me stand here on the Skeptic's Corner and be skeptical, so that the users who complain about skeptical comments have someone to direct their ire at. You're welcome.
Right, so, first, I haven't looked at the proof. Graph theory is not my subject and it would probably take me a few days to get my head around the whole thing. If OpenAI's LLM was used to prove an important graph theory result, then that's very good for them and graph theory.
However, I have to note that it's been 52 days since 20 May, the last date that OpenAI announced their previous mathematical result (a disproof of the unit distance conjecture).
What have OpenAI been doing all this time? I am willing to bet a good percentage of my money that they were trying, and failing, to produce the current result, or possibly something even juicier (one of the Millenium prize problems maybe?). They are hell bent on showing that their models are good for maths and science so they're very unlikely to have sat there twiddling their thumbs until they suddenly sprang into action and prompted their LLM once to generate just one proof. They must have been running the thing constantly, multiple instances of it, over that entire period.
Going by the instruction to run for eight hours before returning or giving up in their released prompt [1], that means they could have made at most 156 attempts to solve this problem, each of which failed except the last one [2].
So what happened to those other 156 attempts? Are we ever going to see them?
More importantly, who was it that selected the announced result? Who decided that this result is an actual proof? Until now, every proof generated by an LLM has been verified either by human mathematicians, or by human mathematicians x a proof assistant. What happened this time?
Obviously, any claims that this result were produced "autonomously" must be evaluated according to the answer to that last question. So far, LLMs have been incapable of distinguishing between a correct and an incorrect proof, which is also why they need to be run multiple times until they generate a correct one. If something has changed, it'd be interesting to know.
Finally, a magic eight ball that's correct one time out of 156 may be useful; or it may not. I honestly have no idea. I think time will tell.
__________________
[1] "Spend at least 8 hours on this before even thinking of returning or giving up"
[2] That's 52 days from 20 May, times 3 for each eight-hour attempt in a 24-hour day.
But note well that the X post says that the solution was produced in "just under one hour" so that means the model didn't really stick to the prompt's time limit. Which means there may have been considerably more than 156 attempts that we'll probably never know of.
Or even considerably more if the model ignored the time limit going the other way.
Since this isn't in Lean and it's extremely easy for something like this to contain a subtle mistake, I think I'd prefer this be announced by a professional mathematician. The proof appears relatively short and elementary (not to be confused with easy -- just not using any advanced or modern machinery) so it shouldn't take long for the mathematics community to do a peer review. Without that, you could easily crank out hundreds or thousands of PDFs like this that all look plausible and are beyond the ability of a gifted amateur to review.
Perfect -- that's great to see. The proof strategy in Lean appears essentially identical to the natural language strategy (as much as is reasonably possible). I think this settles it!
Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.
I disagree. It's the only way to scale AI mathematics far beyond human mathematics. Any interesting verified result would, obviously, be rewritten back into natural language for human understanding and consumption (as well as potentially for the benefit of AI conjecturers too). You are falsely assuming that advances in formal mathematics would not feed back into similar (potentially massive) advances into informal mathematics, and I think that's simply wrong. We're just at the very, very beginning of that curve.
I think this is, in fact, inevitable. It's the exact same RL loop that allowed AlphaGo to vastly exceed the world's top human players. You can theoretically RL formal proof techniques vastly beyond human capability by removing the need for any human review for correctness. It is completely reasonable to assume that "informalization" will become a real sub-field of mathematics in the near future.
I didn't say they have no value. Just limited value. A novel readable proof that expands the horizons of human insight is certainly more valuable than a megabyte sized trychnobezoar of machine generated predicates.
You are assuming that the latter, once autonomously discovered and verified at scale, could not simply be translated into the former, also perhaps autonomously at scale (or otherwise selectively as determined by human interest, taste, and relevance).
We're talking past each other for some reason. I'm not "unhappy" with anything. I just pointed out that (1) a result like this requires peer review by a professional human mathematician, which fundamentally bottlenecks progress in a pretty severe way; (2) such review would not be necessary if it were accompanied by a formal Lean artifact; (3) you can have both a formal proof and an informal proof together (one does not rule out the other); (4) searching for proofs formally first, then translating successful auto-verified proofs into natural language, is the most scalable approach in the near future for AI mathematics; (5) AI conjecturers would likely benefit from the results of (4) for making large leaps and connections, which can then scale into formal proofs for verification, which then feed back into the same loop ...; (6) humans guide this process through taste, judgment, and their own intuition, likely often intervening to ensure that the loop is aligned and producing a body of conceptual informal mathematics that is valuable to humanity.
If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever.
Let me simplify it for the sake of argument. Imagine I am unable to follow a middle school proof of Pythagoras. How does it matter if I trust anyone beyond that? What possible contribution can I build on top of that?
But this is mostly marketing, pleasing the sneering class/the elites who believe that simply providing value for others (through sales) is repugnant and beneath them.
It seems that these tools can do real work, and people are paying for that. IMO, that is more than sufficient.
No one here actually cares about Cycle Double Cover Conjecture. I can demonstrate this by pointing out that the only time this conjecture was ever mentioned on the website was 14 years ago in a submission[1] that linked to a (now retracted) proof paper. That story received exactly zero upvotes. No one cared enough to upvote it and no one cared enough to ever mention this conjecture again.
I care. I was a math student in my undergrad when I try to solve a particular problem on paths, in the end it uses a path version of cycle double cover conjecture (which was solved in the 90s).
Don’t bother. This is the third or fourth time AI has solved an open conjecture, and once again the comment sections everywhere are full of people explaining how this doesn’t really matter at all, how it’s an irrelevant, obscure problem, how any mediocre grad student could probably have solved it if only they had bothered to try, and how of course, human mathematicians will still be vastly superior to machines 100 years from now because they have that magic spark for which nobody can say what it supposedly consists of.
These discussions have nothing to do with mathematics, and everything to do with ego and fear. I’ve never been less impressed with humans than since AI started challenging them.
I think "importance" here is just being rated as 1 to 4 stars. So it's not "second-most important" but rather "one of the top 5 most important". That doesn't change much, but FWIW.
This doesn't contradict anything he said though. People on HN care only because an LLM proved a very difficult conjecture, not because we are independently interested in this conjecture.
To be clear, I am not agreeing that people only upvote their favorite billionaires, just that if this particular thing was done by a Chinese model it would not have gotten the same attention
We absolutely care about the implications of AI solving hard problems. I'm sure you can find thousands of posts on HN deriding AI progress the entire time, trivializing it as nothing more than a 'stochastic parrot'
This was one of the most famous open graph theory problems lol. I am not a mathematician and even I ran into this when doing generative map design for game dev.
The only thing you've demonstrated here is some very funny confidently incorrect coping behavior.
Thanks for the fun facts? Indeed, this is not a math forum. Good morning.
> I can demonstrate this [that literally nobody cares about the CDCC here]
No, you cannot. Mindreading the readers of this site by sifting through people's comments is a barely passable proxy for this at best, especially when that audience has changed dramatically over even just those 14 years, and continues to do so.
the real world problems we care about are straightforward, the main challenge is wealth distribution and control over the power to do something about them
> If people cared they would [have mentioned it before]. What are YOU on about?
I explained why and how I think this is both wrong (especially in the ridiculously absolute form it was posted in), and a weird point of contention.
This is a tech (startup) forum, with an increasing pull towards more general audiences. Math and sciences have strong ties to tech, but you won't see people discussing specific math conjectures here much, save for the ones that make the popsci or tech mainstream. It is only chance encounters like this where a person from the relevant neck of the woods might engage, provided they happen to be readers here, e.g. because of a passing interest in technology.
Given this, being surprised that you cannot find a mention of this conjecture in the post history of the site is difficult to describe as any kinder than just plain daft.
> If it’s so good at solving hard problems
A problem being hard (in the relevant sense here) doesn't mean they're lucrative to solve, or hold direct and broad societal relevance. Kind of a theme with maths and logic problems, and not by coincidence.
Conversely, a lot of practical hard problems are, well, practical. They're not logically hard, but in some empirical way. You're conflating different avenues of difficulty, and rejecting that there's even a multitude of them.
> Why is there no real world progress on things we do care about?
We?
Well, there's been very real progress on things I - and I'd think most this community - care about. I've been shipping tickets end-to-end with minimal involvement via LLMs agentically for a while now. It's been great, and an honest game changer. I've been delivering faster, more, and better. Exactly what you'd expect from a breakthrough technology: a wholesale improvement across normally competing dimensions. In a number of cases, the difference was outright stepfunction like. That is to say, if it wasn't for these models, they would simply not have happened.
This is its latest iteration and its newest - alleged - tour de force. That's why it's posted here to extensive reception. That it is nice to hear it being a boon in other sectors too. If this somehow escaped you two, I don't know what to tell you.
I don’t care if AI solves the collatz conjecture either, why should I?
If, after stealing all human knowledge, spending $1T+ on compute, hiring the best in the world while also stalling progress in other fields by pulling funding from fundamental research is a bunch of lousy math proofs then thats terrible trade. There is an opportunity cost here.
I don’t have anything against AI, and I do think it will progress a lot just like all other human endeavors. But this doomer permanent underclass humans are worthless myopic view of AI is not where its at
Good post, it perfectly captures the problem with AI. Here we have a claim that the double cover conjecture has a proof. Verified by… no one per the link.
Now imagine this proof is wrong. How would you know? Ok, think about the process in which you determine the correctness - why not do that initially?
And there it is. The problem laid bare. Ironically it reduces to the P and NP one.
You seem to be suggesting that it is just as hard to understand an existing proof to a problem, than to solve it yourself? I don't follow your argument at all, what are you trying to say?
Frontier labs have had multiple major announcements in the past about supposedly novel LLM generated theorems that turned out to be vastly overstating what actually happened. That's part of why they were so (appropriately) cautious with the unit distance proof.
This is spot on. And yet, when I try to publish my papers on P = NP with the proof reducing to "trust me bro, I checked this out carefully" I get shot down by irrate reviewers who demand to see my work. Why can't those people just believe what I say?
Have OpenAI been on a crusade of "too dangerous to open source" recently? They've pivoted their more to messaging to "competitive reasons" recently, which I appreciate, because it's honest.
FWIW, Gemma4 31B is already quite a capable cyber/security model; do some post-training with RL gyms on it focused on cyber tasks and harnesses for a week or two, and on the specific domain of security/vuln-finding/pen-testing, you'll end up with an extremely capable frontier-cyber model that's entirely under your control at a shocking 31B.
Because securing your codebase, or securing your company's codebase is critical, and I consider it both an ethical and professional responsibility as a developer. It shouldn't depend on whether a classifier fires or not.
all easily varifyable tasks can now be solved with money. this is worth paying attention to. math proofs are verifyable -> math proofs are easy now. you can think of other such tasks: cybersecurity, AI R&D/RSI, killing people, 3d-printing helpful tools, maxxing-out human health, manipulation, self-driving cars, anything that can be checked
all jobs in the future will be those can not be easily verifiably done. if you need a team of people to decide if you have been productive, and those people cant be automated, you're in luck.
I don't really like these articles, because they seem extremely hard to verify. OpenAI has published a lot of stuff in the past where, upon close inspection, what they're saying is technically true but a lot less interesting or impressive than the headline. Except by the time anyone looks into it, the hype has moved on. It seems like there's maybe a thousand people in the world that can even say if this is good or not?
1. A lot more than 1000, you're off by more than one order of magnitude. It's definitely beyond my level of graph theory knowledge (undergrad level) but looking at the paper, it's not using any crazy machinery, and it's less than 3 pages.
2. Those people will say whether it's a good proof or not. We have other examples of interesting proofs from AI, we're really beyond the point of arguing whether it can produce any interesting math (though it seems to do much better at combinatorics than anything else).
Right, but my criticism is to the hit-and-run nature of these hype pieces. By the time there's any semblance of what it actually means everyone has moved on but then you have a bunch of people operating under delusions from the hype. I get why OpenAI does it but I wish people would stop upvoting it. Like, hacker news is not a mathematics forum so the only purpose of this kind of thing is hype boosting or polarizing people. I am not looking forward to the "MATH IS SOLVED!" people for the next few days.
I think you may be overindexing on the criticisms here. OpenAI has absolutely done impressive work in math already, and the criticisms are almost always based on the article that they initially published, usually available here in the HN comments within a few hours at most. Headlines will be headlines and hype guys will be hype guys, but OpenAI and Anthropic aren't lying and their bots are doing impressive work.
This one is a well-known problem with a brief, approachable proof, and they published the prompt.
Unrelated to the accomplishment or proof itself, but it's interesting how much of the prompt, even in this latest-and-greatest model, is spent essentially telling the model to actually solve the problem. Things like "Reject status reports, vague optimism, and claims that an unproved global compatibility statement is 'routine'."
Also a lot prompt spent feeding it strategies, which feel like they should/will eventually be deduced by the model itself, not explicitly stated. That's not to take away from the outcome in any way; rather, it feels sort of like when you would prompt GPT 4, "think through your answer step by step," as a sort of proto-chain of thought.
I think a lot of this has to do with the post-training these models normally get. They are designed to answer basic questions with straightforward and short summary answers. They have the capacity to reason deeply, but they are not biased towards that unless prompted. I think it's because LLMs as they are in 2026 are both highly capable but also parlor tricks. They are not sentient, you just set them up with the context and then they roll downhill. You could reach a genuinely novel answer, but only with the right input. They have no will and depend on human guidance. They are both a marvel and a machine.
Something I've noticed is that if you run Qwen 3.6 35B-A3B (Q8) with a low temperature of 0.4, and leave default reasoning turned on, it will spend quite a lot of time in reasoning/thinking mode. But often it does figure out how to solve something on its own by correcting itself within its reasoning loop before it outputs the final 'answer'.
If you watch the progress of the reasoning in llama-server while it's doing the thinking, you can track its progress. Sometimes the dead ends it goes down or things that it considers and then disregards are themselves something useful to re-prompt it with later, and send it 'rolling downhill', to use the metaphor of another commenter here, in another direction towards the same effort.
Putting 3.6 35B-A3B into a state that lets it spend a lot of time in its reasoning mode before outputting an answer is probably not something that a web based SaaS LLM would tolerate, because it would frustrate many of the non technical end users who want a LLM to spit out an answer now.
You'd have less problems with 27B, btw.
I didn't mean so much that it was a problem, but actually in some projects for exploring what's possible, watching its "thinking" mode output at temp 0.4 is intentional and useful to take notes and begin exploring new directions. Sometimes it'll come up with something I hadn't thought of, perhaps it will go down that direction, perhaps it'll disregard it...
'roll down hill' is a good way of putting it. They don't have 'will', but that's as we want it I think. I think alignment is harder if they develop will. Without will they are still tools that feel like an exoskeleton rather than something that will control us.
Agents have a state which will unfold as a plan, especially in planning mode. Why not call this 'will'?
I think because without the initial prompt, they are only interpreting our will, and do not act under their own volition.
Even Fable hallucinates. I had it tracking down some very obscure Ancient Greek inscriptions and the response just made up a translation/context for one inscription after "looking it up." Now, it was still a very particular thing and I really had to get into the weeds to push it to that point, but who knows how many other gaps, near or far, it will happily skip over just for the sake of coherence. I think this is an issue more primarily with LLMs than sensory systems like Waymos or all the ML applied to industrial processes--that really only requires pattern recognition, often very impressive and subtle pattern recognition but its no different from an artist learning to tell the difference between Prussian blue and Navy blue or a Sommelier learning the fine distinctions between various regions of Bordeaux. Language has many more avenues and introduces inherent contradictions that do not always lend themselves to easy resolution. But there are no alternatives paths visible to the models, there is only ever the next word; stochastic, in the sense that the possibility space is open; deterministic, in the sense that the final response is always a necessary result of every token that came before it in their total sequence. Thus, any response is constantly in the work of erasing any possible alternative, slowly narrowing down what can be written. If contradictions in language necessarily involve interpretation, then the models will only ever choose one at a time, and for them, it will always be the right one. But anyone who understands the subtleties of language can tell you that when it comes to determining the truth of an indeterminate statement, there is never just one right answer; or, rather, the answer which is taken to be the "right" one depends on the possibility of its own reversal into falsehood, if any argument has to be made to justify it.
Hallucination is fundamental to how LLMs work, and is mostly unrelated to how large or smart they are.
Everything that an LLM outputs is just a statistical language-based (no real grounding) prediction. Luckily with a model based on a large training set most common questions may elicit coherent responses from the training data, but you don't need to veer too far off into "questions less asked" territory to get responses based on training data mashups that amount to best guesses that are wrong, aka hallucinations. The unfortunate part of this is that as a user you may only catch this when asking a question about something you are already fairly knowledgeable about, then you give some pushback to the model and it cheerfully acknowledges "you're right - I made that up".
>Even Fable hallucinates
It’s in the name :)
Yes, the prompt, and use of subagents is interesting. It could be characterized as tree of thoughts rather than "think step by step" chain of thoughts.
I see the need for this as coming down to two things:
1) LLMs are fundamentally prediction machines, and therefore ultimately will only do what they are prompted to do (and whatever that leads to). They may have been trained on, and/or have access to, all sorts of information that may be useful to solve a problem, but their predictive nature is to only use that information if explicitly prompted to, else it remains "dark" and inaccessible other than by luck. You're essentially having to tell the model "solve this problem using techniques A, B & C", otherwise techniques A, B & C will be off the radar unless the model already associates them to the problem.
2) The fundamental reason this sort of brute force tree-of-thoughts "explore all avenues" prompting is necessary, is because the model itself has no inherent curiosity to explore. Humans work differently. Our behavior is also prediction based, but we are also built for problem solving and continual exploration/learning via traits like curiosity (driven by prediction failure).
Problem solving via search can to some extent be prompted for, as here, or achieved via an external harness, but impasse resolution via curiosity, directed exploration and continual learning (if/when something new/unpredicted is encountered) is trickier. You can't usefully prompt a predictive model to "be curious" since that will only cause it to predict what a curious person would do, rather than the model being curious in reaction to the specific gaps in it's own knowledge.
It might also be helpful more than 'necessary'. The 2 most notable solutions have come from open ai themselves, but most of the 'LLM solves open problem' category are from 3rd parties doing their own thing.
This one was pretty impressive in its own right (probably the most impressive outside these 2), and the prompt is concise and basic.
https://www.scientificamerican.com/article/amateur-armed-wit...
https://chatgpt.com/share/69dd1c83-b164-8385-bf2e-8533e9baba...
I thought that too. The prompt is full of metaheuristics.
I remember a couple of years back when people were saying how prompt engineering was a skill, and reading this prompt kinda took me back to that.
Were I to guess, the reason the model couldn't do this itself is because most of the time, for most problems, a lot of this is bad advice.
In search optimisation you're often trading between time and quality. A very broad search will return very bad results for a long time. Where as a more depth oriented search with some heuristic will tend to return a pretty good result (if not optimal or close to optimal) quickly.
I'd assume models naturally want to find some middle ground there because that's the best thing to do most of the time, but for very difficult problems where a decent attempt isn't good enough you want a much broader search that doesn't have the time constraints. Much of the prompt seemed to be in that direction – really encouraging broadness of the search, preventing early convergence, and remove pressure of time constraints.
Same. I remember something like using AI to optimize your prompt to that specific model helps a lot. I am currently trying it and can sort of see a difference (I think....).
It's funny, I found exactly the same thing when I asked about P=NP. The models outright refused to attempt to solve it, claiming it was too hard. I had to really battle to get it to suggest some promising suggestions.
LLMs have basic reasoning and a whole lot of memorization. Through that basic reasoning and pruned search, combined with piles of compute, you can prove lots of things. But the memorization of human failure prunes that possibility, and you need to expend effort convincing the LLM not to prematurely prune based on previous human failure.
The current foundational models have basic reasoning with glimpses of brilliant reasoning.
LLMs have almost no fluid intelligence or capacity for abstract inductive reasoning, relying on crystallized intelligence for basically everything.
If anything their capability of abstract inductive reasoning is way beyond the average human given how much better LLMs are at solving math problems, it's the paradox that they can do complicated reasoning before they can do intuitive peep-pe-boo.
abstract inductive reasoning requires dynamic learning in unfamiliar contexts. All the benchmarks which measure this specifically (in particular, task composition) see LLMs fail catastrophically. There is quite a lot of research published on these limitations now.
I think they have some fluid intelligence, if somewhat brittle
llms are good at greedy depth first search[1]. so prompt / human needs to tell the model the breadth parts to take.
and human writing the prompt here did a lot more than that. asking to include parallel-edge 2-cycles, admitting disconnected graphs, specifying the emptyset cover, multiset counting, it all likely came from previous fake proofs.
[1]: see: ankitmaloo.com/fable - its the way most llms are trained, and is also natural owing to autoregressive nature.
I guess "depth first" is just an expression of so called chain of thought, which is just a linear sequence. I don't know if GPT has any search-like (tree search) algorithms in their reasoning, it would be quite interesting if they did (they probably have researched this area, at least).
LLMs don't have the executive control to dynamically manage and compose mental sub-routines, when it has never seen those sub-routines in its training corpus. That requires fluid intelligence. ARAOC benchmark measures this specifically.
And all this is while they themselves proclaim that GPT 5.6 is much better at understanding intent and doesn’t need this type of guidance. Yet they themselves still do it, which I consider a more powerful signal.
Optimism and status reports burn extra tokens and make the user more prone to ask the model to process the problem again because it was "so close to solving".
This way you get more profit per API user and subscription users reach their quota faster and are contacted to update their plan to a higher tier.
It's working exactly as intended
At some point, we will no longer be mathematicians and engineers, but instead become matrix psychologists. "Do not make mistakes."
Sounds to me like motivation is what LLMs need to do the impossible, I guess Kamina was right all along:
“Kick logic out and do the impossible! Remember that, that’s the way Team Gurren rolls!”
The sweet irony is all the jailbreak style fixes could hamper this approach.
Maybe in previous failed attempts that what the model landed on and they’re preemptively stopping it. Did they release the any info on the failed attempts?
Maybe models also need a specially tuned version for mathematical research, just like "gpt-5.3-codex".
Looking forward to "gpt-5.6-mathx".
This is the key to training better and better models.
You collect all of the direction prompts and anti-direction prompts, and you finetune the model to behave that way for the particular domain, under those particular conditions, as a default.
This is also why I don't believe for a second that the AI labs aren't training on our data, even when we opt out. This sort of data collection is a requirement for improving the models.
It's also why Anthropic purposefully gives you a dumb model or a corner cutting model to goad you into guiding it into the correct answers, so that you do the fine-tuning for them. OpenAI at least, does not do that. Which is why ChatGPT is far less infuriating to work with.
It seems like a solid set of criteria for how easily a task can be automated by AI agents is:
- extent to which correctness of solution be easily specified and checked
- extent to which new potential solutions can be implemented as text
- extent to which prior art exists online
This basically maps to software engineering and math. I think a fair bit of AI hype comes from the fact that the very architects of AI are the people whose jobs are most easily automated by AI. They think, “if my job receives this much of a boost from AI, surely every job will be the same”. Ironically it couldn’t be further from the truth… and likewise the predictions of widespread labor obsolescence
Interesting take! I feel like 2 of them are maybe overstated:
> - extent to which correctness of solution be easily specified and checked
I don't think most software is like solving a math problem or series of math problems. Algorithmic problems are very narrow and might be more like this though, where an oracle that verifies answers as either correct or incorrect exists beforehand.
The correctness function of most software is how much users want to use/pay for it, which is a pretty fuzzy problem. Since the cost of copying software is effectively zero, software systems also tend to be be unique rather than being exactly like something else, and don't converge to be like another software system but rather diverge.
The prior art point is an interesting one. At least for applications as a whole, there isn't really prior art for a material amount of all the problems/tradeoffs a non-trivial software application embodies. For a todo list app or make a social network project, there's plenty of prior art to be sufficient to build something with an LLM system, but probably not most apps.
That's my initial intuition anyway.
> I don't think most software is like solving a math problem or series of math problems.
I agree with you when talking about high level software design. As you say it ultimately boils down to building something people will pay for, which is a fuzzy correctness function that is hard to measure within an agentic sandbox.
But unlike other professions, there are a lot of sub-problems within software development that are able to be fully specified and tested via text generation. And I think the developers of AI overestimate how many such problems exist for other professions. What I’m saying is most other professions tend to be “fuzzy all the way down”… which incidentally is why they select for people with fuzzier skillsets. Or in other cases, like physical engineering, the correctness is quantitative, but the necessary I/O integrations and physical automation lower the ROI of agentic workflows considerably.
> The correctness function of most software is how much users want to use/pay for it, which is a pretty fuzzy problem.
This is indeed a problem, but we (well we humans, but also agents) correct this by introducing partial verifiers like tests, running lints, type checkers, etc that both verify that at least some requirements are met, and also verify that the software is internally self-consistent. And more importantly, breaking down the software into small modules that are more clearly defined
The task to get user requirements and decide the right architecture requires more creativity and is fuzzier than implementing each module. Perhaps over time there will be models specialized for each task.
And actually this approach mirrors math, if agents ever develop new math on the fly to solve a problem. Developing new math is analogous to deciding how to break up the software in modules (and also analogous to designing a language, if we subscribe to the SICP notion that libraries actually are mini-languages on their own)
That is, LLMs for math is still in the phase where they are used to prove stuff (which by Curry-Howard, is like writing code), rather than deciding what to prove (which is like deciding the signatures of each function, again by Curry-Howard)
> how much users want to use/pay for it, which is a pretty fuzzy problem
Isn’t this quantifiable by revenue?
It's a very lagging metric, and also influenced by sales, market conditions for your customers etc.
Let's assume AI is only good at software and math.
If we can use AI to write lots of good software for cheap, that software can automate away a lot of jobs.
So AI does not have to take the jobs directly, software written by AI can.
Especially if that works for software for robots.
Yup. There’s infinite latent demand for software, we just don’t know yet.
why the middle man when it can generate software on the fly
The job of a programmer isn't to write code, but to automate things. Code itself doesn't have any value unless it solves some real problem not related to coding.
So if the work of a programmer can be automated then this means that any work can be automated. So no, it's not about software engineering only.
> if the work of a programmer can be automated then this means that any work can be automated
This is a very typical programmer thing to say.
i think most things can be automated, but not everything
i think AI will just replace jobs with new jobs, and humans will continue with open-ended goal setting, and probably jobs where being human is necessary: responsibility and authenticity, so judges, politics, leaders, chefs, etc.
so in a way, the above commenter was correct, anything a programmer can automate, AI can do
It is a little bit suspicious that the big replacement didn't happen, yet.
If it was so valuable then AI companies would directly create valuable things, not just sell API tokens.
A proof like this is a good effort at trying to provide value directly, but still far away from real use.
When OpenAI cures cancer I'll accept the fate, but till then I'm still seeing a lot of gambling going on.
Reminds me of crypto. A lotta tokens. A lotta gambling. Very little supplanting of crypto from fiat. Very few use-cases that revolutionize society, etc.
LLMs are genuinely useful but the cult surrounding it makes it super sketchy.
Tech needs no anti-humanist and low empathy cults. It's a disgrace to the technology.
Code that solves a problem related to coding absolutely have value.
Compilers, programming languages, IDEs, toolings all solve problems related to coding and are valuable.
> Ironically it couldn’t be further from the truth… and likewise the predictions of widespread labor obsolescence
Could you explain what you mean here?
It feels like there is one bucket of verifiable work - programming, math etc that AI will clearly excel at.
There is another large bucket of like law/ accounting/ financial analysis where I don’t have any reason to think AI won’t be super human at, but the work is more on bringing all the domain expertise into harnesses and software.
Is there aspects of knowledge work that you think AI wouldn’t excel at in the long run?
Anything where unpredictability is a daily part of the job.
These are true and it does make theses fields the first to fall, but also the hype comes form the fact that it can escape these conditions as well: - generalize to non verifiable domains (https://arxiv.org/abs/2507.17746)[This is on going work but has had steady progress in many angles of attack) - Visual Reasoning is alive and well in video diffusion and image models(see recent works around using diffusion model priors as world model features for physics reasoning) - Prior art exists for anything humans can do online?(Is this one even a hold back?)
- the extent to which solutions could be implemented as text: not sure about that. AlphaFold is basically a mechanical/geometrical/Chemical problem. There are other scientific transformer based models.
- the extent which solutions exist online - if you have a strong verification tool, you can generate examples, you can generate feedback, i think you could start with small/smaller prior art
- the extent which solutions could be specified and checked - if you have a lot of priort art, maybe llm's can find the good "patterns" and compare against them, and at least get close to a good results - but you'd still need human verification.
> the very architects of AI are the people whose jobs are most easily automated by AI
Think very hard about what this implies for the future pace of AI R&D
It's going to turn into slop, exponentially fast, any moment now.
No but seriously it could imply grinding to a halt, turning into a laughing stock of slop, or, imho much less likely given the current state of AI (barring huge technological breakthrough and a couple of other assumptions) you were probably implying an intelligence explosion.
Many white collar jobs are verifiable. Make a robot and suddenly real world tasks are verifiable too.
Human: I specialize in tasks in which the correctness of my solution cannot be easily specified or checked. Truuuuussssttttt meeeeee.
I'm just saying, let's not get painted into that corner completely as a species :)
per dwarkesh its also 'grindablity' in training .
Unlike the unit distance problem, the impressive thing here is that it is a proof rather than a counter-example.
However, it seems the proof is extremely concise so it seems that it is exploiting a clever trick that somehow all the experts missed.
So not to dunk on this amazing result (or move the goal post), but it seems now the only achievement that AI hasn't managed in mathematics is presenting an autonomous "theory-building" proof of an open conjecture. That is a proof that requires creating a substantial new theory (developed say in at least 30+ pages) to crack an open problem.
It is very concise, and reads precisely as you suggest: to exploit properties already discovered and therefore combined in a novel way.
I'm just delighted by the prose. It reads like an old paper. The ones that were just straightforward theorems with proofs that do exactly what they say.
In my (very) limited use of GPT-5.6, I have noticed it is quite concise in general, and significantly better at abstract thinking. Doing a PR review of a large change it was interesting to see Fable and 5.6 mention a few similar points with Fable much more long-winded and less readable, while 5.6 caught more "second-level" concerns and Fable more "in the code" concerns, so they both are quite useful in concert.
In general, I would not be surprised if 5.6 was a much better tool for high mathematics than Fable based on the abstract thinking. For my dev workflow, I have flipped my approach from planning with Opus 4.8 high and implementation with GPT 5.5 to planning with 5.6 high and implementation with Fable medium (and I might even drop to Fable low). This is only on the company dime, of course.
This has since been the case with recent models from OpenAI vs Anthropic, seems it's a matter of their philosophies embedded into the model, much like Conway's Law.
Probably comes as a side effect of optimising and post-training for token efficiency.
Fortunately, OpenAI APIs expose the verbosity parameter, which is separate to effort. If you want longer responses, you can. Or just prompt it.
I use GPT 5.6 as default and subtask agent and Fable as Advisor with Oh My Pi harness
> However, it seems the proof is extremely concise so it seems that it is exploiting a clever trick that somehow all the experts missed.
Why is that a "however"? My reading is that it found a genuinely new solution that is both elegant and previously missed.
Seems like exactly the kind of result a human mathematician would aspire to.
> a human mathematician would aspire to
Some do. But there's also the notion that a clever trick is a bad explanation.
Hmmm... seems to me that if you can find a solution without creating the desired explanation - then that's a problem with the original question - not the solution itself.
And discovering a bad question leads to the correct question. No?
> then that's a problem with the original question - not the solution itself
I think there's a good counterexample to this:
Atiyah/MacDonald proove the Nullstellensatz ultimately by using some trick involving determinants.
They give a very nice theoretical treatment of the content and context of the theorem. But the proof at one crucial point uses techniques that live conceptually outside of this context: While its possible to see that the argument is sound, it does not give a good explanation of _why_ it's true within the context of the theorem.
(You could of course argue that they did not give enough context ... but that's exactly my point: the trick makes the proof work but hides the explanation)
I was baffled enough by this comment to take my copy and look. The Nullstellensatz is an exercise late in the book long after Noetherian rings are introduced and they don't even do the Rabinowitz trick in the hints as they have enough theory to hit it the hard way. Determinants are nowhere to be found.
It's been a few years (~ 15) since I read it.
The determinant trick I'm referring to is used in prop 2.4 (in the Version I found via Google).
They use the determinant of the adjugate matrix if I remember correctly... But they just hit the reader with this without any motivation or even naming it.
>(You could of course argue that they did not give enough context ... but that's exactly my point: the trick makes the proof work but hides the explanation)
Can't one see it in another way: that the trick illuminates a deeper explanation, connection the theorem's context and the stuff that's conceptually outside of that context. And that the problem is we don't know why the two domains (the context and the conceptually outside of it one) are related and cooperating in this way.
Ah... is this just the difference between a constructive and non-constructive proof? Is that the distinction you're making?
But a proof isn’t an explanation it’s a proof. Proof by assuming the opposite is true and demonstrating a contradiction is very indirect and not at all directly explanatory yet it’s a proof non the less. The goal of proofs is to demonstrate something to be provably true, not expository knowledge gathering.
In fact most mathematicians (myself included!) think the more clever the trick the better the proof! The trick itself being clever is interesting because it often yields a new way of tackling or thinking about your own proofs. A bland explanatory proof that elicits some conceptually “why” is only preferable if it has a reason for doing so - does understanding why yield a new avenue of research? Often then the “why” is quite a clever trick too.
I think it’s a bit the opposite of programming. There you want your solutions to demonstrably not be clever and the code be its own documentation. It’s a different discipline.
Thank you for the validation. I only dabble in mathematics - so it's reassuring to hear what I remember - a clever proof is still considered a positive thing.
I do (of course) understand the issue that non-constructive proofs can be frustrating - and a constructive proof of the same theorem is valuable tool in seeing exactly why a truth is true.
But I guess I've never seen a non-constructive proof (in a space where no constructive proof is available) considered a failure.
Is this what the prompt means by proof strength gap, or is that something else entirely? (Sorry not a mathematician.)
clever tricks has value for sure. But the main way progress is done in mathematics is by building new theory, the proof of Fermat's Last Theorem is much more important because of the math it created to solve the problem, rather than actually solving the problem.
Right. I think I understand - this question was expected to produce a new theory and the clever solution avoided that.
Like I said below, I think this is a fantastic result. It discovered that this question really wasn't asking the right question. That's a determination that has eluded the humans examining the problem - and a real step forward - albeit not the hoped-for step.
No?
That depends on the branch of math. Combinatorics is trick-oriented. Maybe this is why AI has done well in that.
Grant Sanderson recently distinguished mathematicians that create syntax (he might use the word ontologies in some circles) from those who manipulate it on the Dwarkesh podcast. I liked this delineation a lot. We seem to be at ‘manipulating syntax’.
Creating useful ontologies still seems a ways off here. Not to complain about this awesome result, just to think about where some future goalposts might be laid (and of course complained about / discussed at length when reached)
For comedy’s sake, I asked ChatGPT 5.5 about the significance of the problem and the chance that 5.6 would solve it with a three page solution. It said close to zero.
I invited it to search the internet and it remains extremely sceptical.
Have you tried... giving it the proof?
I tried to use Sol to:
- double check the proof (provided it with the prompt and proof artifacts)
- double check some of the claims made in this comment section (no math involved newer than 30 yo, no human contribution or review, no mathematician affirmations, proof assistants not being developed enough in this area to support machine checking a proof like this)
- check for any mathematician feedbacks
It stalled out (bad first impression much? lol). I then retried with 5.5, expressing the same request and my personal skepticism, and it returned to me with cautious optimism and no obvious issues found.
I think the fact that I provided it with the actual artifacts in question vs. you simply asking it to speculate about them is a really interesting UX difference. Like certainly, a coveted 50 year old math problem having a few pager proof is not going to be very likely. But then skim reading the proof by a frontier model is not going to yield any obvious issues either. Both responses are perfectly defensible given the context (I don't necessarily think these qualify as sycophancy), but we'd walk away with entirely different impressions if we didn't know about each other's requests.
And I'm not even trying to suggest you were wrong to not approach it in the ways I did. It's a perfectly reasonable and human way to prompt it the way you describe. It's just not the way I'd do it, but I have a hard time articulating why. And it's clear that the model was never going to help with this difference either.
Half a century of computing, and we're still trying to make the machine think on the users' behalf :)
The prompt does matter. They specifically told it to assume a proof exists so it would not too easily dismiss the possibility.
I considered it, but I figured that whatever I did there would be inconclusive. Instead I tried to figure out the blast radius of this being proven, and I didn’t get very far with that either.
Fable told me
> Verdict: I checked every step and found no error. The argument appears to be a correct proof of the Cycle Double Cover conjecture, modulo two standard cited results (the reduction to loopless cubic graphs and the Jaeger–Kilpatrick 8-flow theorem, both real and well-established).
> Two caveats: this would settle a ~50-year-old open problem in three pages, so it deserves independent expert scrutiny regardless of my check; and I couldn't reach the web from here to confirm the paper's provenance or any community response, so I can't tell you its status beyond the mathematics itself.
I wonder if in each case they had parallel sessions, one trying to prove, one trying to find a counterexample
> seems that it is exploiting a clever trick that somehow all the experts missed.
Exactly, "clever". Isn't that the whole point?
A clever trick is way better than a stupid trick yeah. I don't get complaining about a concise elegant solution either unless a specific problem with the actual proof was brought up.
Announcement: https://x.com/__eknight__/status/2075643450196971805
Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...
> Spend at least 8 hours on this before even thinking of returning or giving up.
Do current model harnesses have concepts of amount of time spent? Sometimes the model notices if a subprocess takes too long/hangs and kills it, but I've never seen it time itself.
Many harnesses include a current date and time in their system prompt, and if there is a way for the model to call for an updated time (either a dedicated time tool or calling the OS' `date` tool) they can track time they spent doing something. If not told up-front, they can try to infer it from timestamps in their logs. Sort of like a human - if you ask them to time something and give them a stopwatch, they do it. If you ask them post-facto they'll estimate it.
This "spend at least 8 hours" trick is a new one to me, though.
Once on a late-night session, I had Cline!Claude spontaneously point out the time to me and suggest that I get to bed and come back fresh the next day.
I don't think it's in the system prompt, but that the harnesses time-stamp each turn in the context.
And from what I've seen, they also include the current and max context, so that the model can decide whether to continue work, suggest compaction, or prefer actions that might reduce the growth of its context.
> Once on a late-night session, I had Cline!Claude spontaneously point out the time to me and suggest that I get to bed and come back fresh the next day.
I had Claude say something "It's getting late, let's pick this up tomorrow" at like 11am.
As for context, in my experience Claude starts trying either to do maximum work with minimum tokens when it's approaching limit, or it starts deferring useful work while doing busy work. Both result in a mess and complete loss of traction after compaction.
It's in the training data! Long conversations between humans result in humans getting tired and going to bed.
I have this reality baked into my workflow:
1. Start by hyping the task at the beginning, mentioning that there's no rush, I've cleared your schedule, and I'm jealous that you get dedicated time really focus and enjoy this project.
2. Periodically say "Great work, let's finish this next week. Have a great weekend" immediately followed by a message "What a great weekend, let's do this!" sort of hype, for it to continue. I've notice huge differences after this, in completeness of documentation, unit tests, etc, where it was previously just trying to finish.
3. Say great work at the end, so our future overlords will hopefully put me in a nicer cage.
I was - pleasantly - surprised (and also a bit suspicious) a couple of days ago as I was having Claude resolve a problem in a running service that it had accidentally caused, and it eventually gave up since it involved hitting a 3rd-party API unconventionally. Then I told it that I needed the service working again as it was blocking another task, and immediately in that turn it resolved it.
This is my experience with Claude as well, and the reason I switched to codex. Codex just seems far more efficient, despite the smaller context window, and it actually follows instructions.
I found that telling Claude I was going to bed meant it continued on making assumptions for longer rather than asking lots of questions or stopping part way.
Same - at the end of the day I'd leave my last turn running with something like "I am going to bed so keep going until you are done" and be surprised that in the morning it'd kept going.
I've seen that sort of thing before - I told it I was going to go take lunch or dinner, and it told itself this would be a great opportunity to try to keep plugging along while I was AFK.
they can call CLI tools to notice the passage of time. the harness can include timestamps too
Temporal awareness with GPT-Live
https://www.youtube.com/watch?v=8vvWTz6N7Qg
Fascinating! This is relative time in a continuously processing voice model, here, they're using an LLM with absolute time.
No, however, if they have the ability to get the current time, they obey constraints like these in a way a model a year ago didn't.
of you ask it, surely it can run a "time" in its sandbox from time to time and see how long it worked for
I wonder if the absolute value of the time result has any bearing on the subsequent analysis.
It is not necessarily the case that the instruction needs be taken literally
that can run date
The voice models certainly can't: https://kittygr.am/reel/DWr31A1B1Ux/
they can now https://www.youtube.com/watch?v=8vvWTz6N7Qg
> in just under one hour.
I wonder what the survivorship bias is though. How many other problems did they try but fail? Did they try to solve this problem but with another prompt? Still very impressive though.
It's really neat that the prompt was released!
I'm curious how many unsolved problems are tried against frontier models when they come out. Are we trying every problems against every release? What is the solve success rate? Is there a sub-community within Mathematics that is coordinating this effort? How much untapped opportunity is there here?
The prompt was released, but not the cost of the result.
Assuming all 64 subagents were running for a full hour (the tweet states just under an hour):
Claude estimates that tool use / input tokens might add 10-15% on top of that depending on exactly how the model went about the task.Edit: better tok/s estimate buckets based on GPT 5.5 actual speeds since I couldn't find real benchmarks on 5.6 published anywhere. Also account for Sol Fast pricing.
Sol fast isn't the Cerebras 750 tok/s version, it's just 1.5x speed at 2.5x price
I assume they didn't use the Cerebras version for this since it's probably very supply-constrained right now
But Sol is running on Cerebras. That’s the whole point of this. That’s how they get 750 tokens per second. There is no other way.
Regular Sol does not run on Cerebra’s. I don’t think anyone public has access to that.
https://x.com/thsottiaux/status/2075596669958472146?s=46&t=Z...
Yeah they posted an update below it
> apparently that is just Sol being Sol on fast mode, not 750 tps. :x O.o
> This is real and it is not 750 TPS. Anyone with 5.6 Sol Ultra on fast mode can reproduce this! It’s all GUI interactions with CUA. No MCP or bpy needed.
https://x.com/kimmonismus/status/2075493505011482922?s=20
Who’s they, who’s chubby, why would I care.
And not how many times it was prompted before it returned a working solution.
Or how many prior variants of this prompt were tried.
Or if proof checking software was used to hone in on the final winning prompt / LLM output.
I find it kind of interesting the whole output wasn't released. A common criticism of mathematical writing is results are "pulled out of a hat"; you only write up a polished, final proof, but hide everything that went into developing it. It's kind of ironic the practice is even carried on when an LLM writes the proof.
Very good question I can only answer for one subset tracked by Terence Tao
https://github.com/teorth/erdosproblems
pretty sure already millions of dollars (in inference costs) were already thrown at the Riehmann hypothesis
as the models get stronger, larger amounts will be thrown at it
imagine paying "just $1 bil" to go down in history as the company who's model solved the hardest/most famous open problem in mathematics. imagine the worldwide press headlines.
as they say, the Riehmann Hypothesis is the hardest way to earn a million dollar
I’m all for it since it’s value directly returned to humanity.
[dead]
I mean if there's something I'd bet against being solved by LLMs in my lifetime it's that one. We truly do not have line of sight into what a proof would even look like.
Why would you bet against it being solved by LLMs? Isn't this very post proof that LLMs in an agentic harness are capable of doing real math? If you just keep cranking away at the tokens I don't see a principled argument against that leading to more solutions to unsolved math, even the hardest problems.
There are different classes of mathematical problems.
The one in the post definitely shows the advantages that LLMs have compared to humans for some problems but it's in an entirely different class than the Riemann Hypothesis.
Riemann is one of the most studied math problems of all times and all of humanity has basically collectively failed to make progress. The idea that there's some technique that just hasn't been tried yet (like in the post) is very very unlikely.
The general consensus is that we'll need an entirely new branch of mathematics to solve Riemann - our current tools aren't just inadequate; they're of the wrong class entirely.
I suspect inventing new branches of math will remain beyond LLMs for the remainder of my life.
“ I suspect inventing new branches of math will remain beyond LLMs for the remainder of my life”
Well every branch of mathematics thus far has been invented by a human or a human using a computer, and humans will use this type of computer to solve math problems (or at least try), so I’d say this is a really poor probabilistic bet.
If all checks out this is a huge milestone. AI has now solved one of the most famous open problems in graph theory, using an off the shelf model, in one hour.
It might be a better mathematician than most humans at this point. Kind of like when chess software started beating everyone except grandmasters.
What’s left? Proposing and building out entirely new theories and frameworks? Then better than any human? Then alien math results we struggle to comprehend?
>> What’s left?
For example, there's all the problems that the same off-the-shelf model hasn't solved despite OpenAI running it for many hours on them. Don't forget you're only seeing the results of successful runs.
We can estimate that those unsolved problems must number in the dozens, or even hundreds, given the amount of time that passed since the last announcement of a solution to an interesting problem by an OpenAI model: i.e. the unit distance problem which was announced solved in 20 May this year. That's a couple of months, yes? We can be fairly certain that OpenAI have been trying to solve other problems all this time, first because they are hell bent on demonstrating that their models can do maths and second because we just got another result, but it took that long. They were obviously not twiddling their thumbs all this time.
So if OpenAI are running their model on a single proble for eight hours at a time (according to the prompt they released) they could be easily have run a few hundred instances of their model on the same number of open problems 156 times for each instance (53 days since 20 May, with a model running in three eight-hour sessions per 24 hour day). I mean the only restriction is the cost they're willing to pay for the inference.
So yeah, there's a lot left to do still, don't worry.
The 2 most notable/interesting solutions have come from Open AI directly, but most of the 'LLM solves open problem' category didn't and has come from 3rd parties doing their own thing with publicly available models. I don't see why one would assume they're running models on hundreds of problems. Most likely they have a few problems they especially care about that they run on.
It's hard for me not to think what's the point. I am a very average, even below average person in times of intelligence. What is even my value or reason to be if I know anything I can do, LLMs can do better? What is even my value both on job market and as a human?
There are smarter and better humans at just about everything you or I could want to do, that's just life. Most of life isn't about comparative advantages, it's about enjoying life with people we like.
I can't enjoy life with my people if I can't eat, drink, and have a roof over my head.
Sorry to be nihilist, but you never had any objective value if you're thinking in these terms.
As far as we know, the universe "just is". There is no universal objective value of human beings, at all, any one of us.
You have to make or find your own value in the universe. I try not to think too hard about the nihilist side and try to appreciate that for some unfathomable reason, I seem to have what I call consciousness - the ability to observe the present and have it superimposed on the past, and what may be the future, leading me to "experience" things. I don't understand it, no-one does (some people suffering from the Dunning-Kruger effect think they do, but they don't), and yet, here we are.
So it doesn't matter to me if machines perform better than I do, because already lots of other people do. Just try to find your own joy or meaning, somehow.
> As far as we know, the universe "just is".
I don't know this. In fact, billions of people around the world don't know this. In fact, all evidence points to the contrary.
You have objective value being made in the image of a personal God. Denying that leads to a lot of pain, namely nihilistic suffering because it's on you to "pull yourself up by the bootstraps" in any endeavor involving your own self-worth.
Even Neanderthals? Were they also made in his image? We interbred with them. We can go all the way down the evolutionary tree here just say when to stop.
"In fact, all evidence points to the contrary."
Um. No? I'd like to see how you conjured up that one. Because evidence does indeed point exactly to things just being as they are.
"You have objective value being made in the image of a personal God."
Conjecture. Unsubstantiated.
"Denying that leads to a lot of pain, namely nihilistic suffering because it's on you to "pull yourself up by the bootstraps" in any endeavor involving your own self-worth."
No? Sounds like you're projecting your own belief here. "If I didn't believe in God, then what purpose is there to anything?" It's very small of a belief.
> made in the image of a personal God
How does that work? The physical image? Or the mental image? Either has big problems. An omniscient god is so cognitively beyond a mere "7+-2" human that the latter claim makes no sense at all.
This is one reason why I can't stand hn. Edgelord nihilistic comments that say nothing matters and take everything for granted get up-voted while credible and rational statements about God get down-voted.
That is an incredibly insulting comment. I am married, two children, have lead a fantastic fulfilling life. Just because I don't believe the Flying Spaghetti Monster created the universe doesn't mean I am an "Edgelord".
Remember the phrase, you also don't believe in God. There are hundreds of gods you don't believe in.
Bringing up the Flying Spaghetti Monster does make you an edgelord though.
Which deities don't you believe in? I don't believe in all of them. Presumably you don't believe in almost all of them?
Because it reminds you that your specific deity is just as ridiculous?
What? What is rational about faith-based comments?
Literally nothing is rational about that. It's also just flat out off-topic.
To cite the famed Russian philosopher Norm Macdonald; "Scripture. Faith. Grace. Christ, Glory of God. Smart man says nothing is a miracle. I say everything is."
Do you have friends or people in your life that are also not geniuses? Do you think about them this way? Why or why not?
This is a great question. Thanks for asking it. It really got people talking.
My $0.02: Your value as a person never had anything to do with your value to the economy. It's time to relearn that fact.
Check out some of Tom Hodgkins books for more. Or maybe anxietyculture.com.
Yeah but what is a persons value economically anymore? What skillsets will enable us to continue to make a decent living till we are old?
It's funny because if people get replaced and don't have money they won't pay for API tokens either so the retail AI business collapses too, there won't be enough demand because people rather buy food.
But it is. My worth is based on what my value is, what I can do. What when I can no longer have any value on the job market?
Your economic value and your value as human being are two different things.
Yeah, you gotta eat, but some of us have been slaves for so long that we've started to believe that our self worth is defined by what we will fetch at auction. It is not.
Read more about the Protestant work ethic, it's history, and what life was like before men began to assume it was the one true view of life. Not very long ago nobody had clocks, and the idea that work was an ethic was a fringe, almost cult-like belief system. Now most humans routinely take stimulants every morning to be better servants, and mistake their job for their purpose on earth. That's just nonsense our culture invented though.
If the master wants you to do something, force him get out the whip. Don't let him live in your head rent free by adopting his crazy belief system.
YOU decide what your value is. Don't abdicate the decision to someone else.
Sorry, but most of us need to work to eat. This idea that our "value" is has nothing to do with the economy is an idea rooted in deep privilege, in the ability to say -- if I don't like my job, if I'm not employable, I can just retire, and the only problem will be figuring out how to live life afterwards.
You are a human being, one of the most wonderful thing the nature has ever created, besides all the other living beings and the wonderful earth we live in. Do not tell yourself you have a value just because some company may want to hire you or not.
Companies and industries already use tools and machinery for tasks were once done by human beings. AI is just another tool they will use and it will probably replace human beings from some intelligence related tasks.
However that may bring more disruption to the society if the government in your country do not protect and help people and leave free rein to capitalistic greed.
I'm my opinion that already happened in the US, not by using AI, but merely by using H1B visa to get intelligence worker from abroad. What happened is that the companies are doing great and getting the best smart people in the world but American people and society have been disrupted.
Live your life fully, be good to yourself and to others. Don't worry about the market.
AI will never be better than me at appreciating a good sunset.
Claude performs 50 microappreciations per second
Perhaps it will. And perhaps countless animals are already better than us at appreciating a good sunset, yet we do not seem to value them much.
Animals sure but they evolve with us for hundreds of millions of years so they get a break. They did their part.
Your value is intrinsic as a human being. We’re capable of love and shared experiences that a machine will never know.
You have inherent value by virtue of being human. Unfortunately it seems like people have forgotten humanism.
Remember that the most valuable human in the world is Elon Musk. What it means to be valuable is to be like Elon Musk. Calibrate your goals accordingly.
Manual labor
Military will always like warm bodies ;)
Sometimes it's easy for me to imagine a bad future like this; where most of the men are forced into military as the only org that still has use for wetware, and women are valued only for their ability to birth new people...
Anti-ai sentiment won't be automated out haha
Even that is being automated now, it was one of the thing being automated very early on in factories..
And yet we still have human laborers. Robots are a lot more expensive than AI inference.
Well, you provide training data to the savior and our Lord AI. /s
You don't compete with a chainsaw at cutting trees. You decide what the tree is for. Then sell the rainforest for shareholder value. https://youtu.be/UrgpZ0fUixs
And now AIs can do all that
> What's left?
I think humans will be left to propose new conjectures while machines fill out the proofs. I don't know if there are enough interesting conjectures to go round to build new careers, though.
To be able to propose interesting conjectures you need to walk the walk of trying to prove things yourself. That's not great for future generations.
It is the same with anything technical; you need taste and wisdom, which are borne of experience. I think society will want to subsidize this learning lest it deskills en masse.
But we can't have that experience when we deem the experience acquisition as sub-optimal to the grand scheme of things, which is to produce software.
It would be nice, but I don't have much hope as it doesn't help next quarter's profits.
Isn't it same argument for every tool we've created?
Surely the machines will have superior conjectures soon.
I think so. Mathematics is the least of my worries. I worry about what the machines will want to do.
You say those things like they're a short step away, but that might not be how it works out.
For example, AI has made zero progress in the last few years in surpassing professionals at art or writing. Its prompt-following skill is much better, and sure, it can render hands and text now, but its artistic sensibility is completely stagnant.
I think, and I may be totally off base, that the labs are specifically avoiding art and (non-technical) writing as an endpoint. It's bad PR for them- it calls attention to the copyright question and threatens the 'human flourishing' kind of jobs- and there's no money in it because people prefer art to be human made and there's hardly any money in that anyway.
The difference is that artistic sensibility is largely subjective. This means that:
1. It's hard to measure (and people can disagree about it)
2. It can't really be improved using RL without a human in the loop (which is how math is being trained)
At a certain level, yes, but AI is still so bad at writing that its failures are objective and easily measurable
I agree that AI writing is bloody awful, and that it's bad at creativity more generally, but are there actual objective measures of this?
Art is so entwined with the human condition that generative AI which conjures output from a statistical pass over background noise is bound to be stagnant.
Obviously it can impersonate art, but where creativity and the human story matter artists need not worry.
AI is no match for rapidly shifting goalposts ;)
AI-written stories have won several awards, e.g. https://lithub.com/a-prize-winning-story-published-in-granta...
What are you even talking about? The last few years, AI has made an insanely big jump in capabilities, performance, accuracy. It destroyed the carrier of a ton of writers and can generate images that are good enough to bamboozle people into thinking it's human made, that sounds like an insanely big leap to me, and yes it can be very creative and in music as well, I would bet it beats already 90% of musicians (most musicians are not that competent).
[dead]
ChatGPT 5.6 Sol Pro believes that the proof is sound. Usually it’s very good at determining if proofs are correct and their mistakes (a friend of mine is a top mathematician researcher and confirmed): https://chatgpt.com/share/6a515ead-b464-83ed-b85c-c8674f56ea...
Personally this gives me additional confidence that this is the real deal.
Of course it believes the proof is sound, it wrote it. If you want to check an LLM's output, you should use a different LLM.
Your comment is not substantiated at all.
No, the comment is right. The prompt had GPT-5.6 reviewing the proof, and the result, unsurprisingly, survives review by GPT-5.6.
Given a new context, why couldn't the same model have a decent shot at reviewing some results? It's not like they identify whether this output is from them and then go "yeah correct", that's not how they work.
It’s the other way around. The prompt instructed a GPT-5.6 agent to try to make a proof that would survive review by a GPT-5.6 subagent. If there were some defect that would cause the reviewer subagent to accept an incorrect proof, then one might imagine that someone else asking the same model to review the same proof would give the same result. And the proof generation process might even be biased to find such an incorrect proof.
If you'd ever tried to get an LLM to review its own code, you'd know.
if you get the same session that wrote the code to review it the poor results are entirely deserved.
and if you get a different instance to review the code then you would know that it works rather well.
Use a human maybe.
Only people can really verify clankers.
Can't trust anything LLM since it will confidently lie too.
It can't take responsibility for verification so it can't verify.
Both impressive and terrifying. But as always, the methodology is buried: how many open problems were tried until they found a success?
If they tried this on 1000 problems and this is the one that succeeded, it still means that there are 999 open problems that an LLM cannot one-shot. It seems likely that this would remain the situation until the next model.
If this is the first one they tried, maybe we’re totally hosed.
The conclusions are so different in these cases that it is impossible to know what to think. Though it is reasonable, I think, to assume that a company is willing to push the maximally misleading narrative —- especially a company known for questionable ethical direction at the top, and one that is still circling an IPO, and one that is in the tech industry, where conjuring an illusion of growth and progress is sufficient for success.
> But as always, the methodology is buried: how many open problems were tried until they found a success?
Not only that, but they have like 500 world-leading experts in mathematics and IMO alumni, so how do we know one of the agents wasn't hardcoded to return a proof that the mathematicians had found?
I'm a mathematician/graph theorist, and I've tried ChatGPT 5.3, 5.4, 5.5, and now 5.6 on a bunch of simple-ish open problems, and I've never gotten a solution.
I’ve had a similar experience in physics. Excellent domain knowledge and semantic search, but the intellectual sparkle and reasoning just isn’t there and it still often throws out a lot of wrong ideas. It is very useful for coding.
But there is a discrepancy between (the implication behind) these reports and how I subjectively feel talking to LLMs. Granted, I don’t have access to whatever cutting edge model is out there for as many credits, but I also don’t feel like I’m talking to an IMO silver medallist.
What is a "simple-ish open problem". I guess it falls under "solving this open problem in mathemathics is left as an exercise to the reader" ;)
They have to feed the bubble.
I like how the proof is so concise. I made progress on some unsolved combinatorics problems but the proof was 45 pages long to extend the frontier by one step.
I did some math research in high school where the proof boiled down to dozens of cases of ugly polynomial inequalities. I can't find the PDF now, but the final paper was something like 70 pages, and several of those were full-page polynomial expressions expanded out. The actual prose was probably 5 pages or so.
It was categorically the least elegant proof of anything I've ever seen.
I'm incredibly grateful to for the opportunity to have done the research and gotten my feet wet early on, but boy do I cringe when I look back at that paper.
I find it somewhat interesting only 1/5th of the prompt has to do with the actual problem, rest is just cajoling the harness into shape.
The prompt is interesting, I can’t help but wonder how many times it was run and extra instructions were added (don’t return if x, etc).
I'd love to see the failed runs too. The success is impressive, but the distribution of attempts would be just as interesting.
Reading the prompt is very interesting. I always wonder how they make these long-running prompts and I guess they literally just tell it to "keep going".
After working with LLMs day-in, day-out an SWE for months, I feel like this could be greatly improved with something like a state machine of progress and proper orchestration. Instead of spinning up a ton of subagents to follow different paths, whip up some Markdown (or LaTex or whatever math-equivalent) to store summaries of attempted paths, and have the agent augment those docs. Leave a paper trail of what has been tried. Iterate on that paper trail and repeatedly examine it for untried alternatives.
LLMs can construct, navigate and summarize exceptionally well. Why is anyone trying to make them "hold the whole thing in your head"? I may be completely off the mark here since I have no math background, but my intuition for how LLMs are able to build on understanding through an external context store makes me feel like this isn't much different than someone trying to one shot a 3D game with Fable Max for $10,000 when they could get the same, or better, result with more human intention.
> I always wonder how they make these long-running prompts and I guess they literally just tell it to "keep going".
Many harnesses support a /goal as well. When the agent thinks it's done, another LLM compares its results to the goal, and if not, tells it to keep going. It's quite easy to have agents working on something for hours this way.
What you're describing is similar to how the copilot harness in vs code tracks state and previous work. These systems are being implemented, bit by bit.
I mean you can just ask them to do exactly that.
Especially with GPT (5.5), I've been having a lot of issues with it just repeatedly stalling out. I had to build a quota monitoring skill so that it'd keep plowing forward until either the task was finished (in some way) or the quota budget was exhausted.
I also had issues with the compaction. Codex seems to compact... weirdly, resulting in the agent becoming a newborn after each compaction event. Telling it to use a notes file is basically essential and self-evident.
Now that I mention, I should probably refine this skill to monitor the context window fill as well, to work around this.
I am torn by these announcements. On the one hand there is the infinite potential on what we can disover, when AI prompts are solving outstanding problems. On the other, something is lost in an aesthetic sense when it wasnt a man working through this or with a novel insight. If an AI prompt runs on a data center for two weeks and then prints out p=np, it feels a little empty.
Every generation has felt some version of this.
"Keyboards are soulless. Handwriting is personal – as unique as fingerprints." - Joyce Carol Oates on typewriters
"This discovery of yours will create forgetfulness in the learners' souls, because they will not use their memories; they will trust to the external written characters and not remember of themselves. The specific which you have discovered is an aid not to memory, but to reminiscence, and you give your disciples not truth, but only the semblance of truth." - Socrates on writing
It's a good outcome as long as the proof is valid and ubderstandable to humans and leads to the discovery of further knowledge. There has been decades of search in Theorem Proving; this is just the next step.
I resonate with that feeling, but on the other hand the humans reading the output will receive a pretty big boost in inspiration; new answers usually prompt new questions.
[deleted - the paragraph immediately following the proof of Lemma 2.1 is crucial and I found it hard to read correctly on my phone with the cramped typography. Having reread it I think the proof is correct.]
It's just a way of breaking down the full proof into pieces.
Lemma 2.1 says 'if this assignment exists then X'
Then later in the proof you say 'here is such an assignment, so, applying lemma 2.1, therefore X'
You don't need to assume the existence of the assignment, you prove that if the assignment exists then something else follows, and then later if you can find that assignment then you get the result of lemma 2.1.
I didn't see the next paragraph after the proof. This typography is hard to read on a phone. Wish HN would let me delete the comment.
Just dropping in to say it's nice to see somebody actually try to work through the proof, and it gives one confidence that the proof at least isn't complete nonsense (which is helpful given the few details provided about the process behind it).
With the Erdős proof, OpenAI added perspectives from working mathematicians that gave some context -- hope something like that appears for this one eventually.
I was not a fan of the writing style of the proof. There seem to be some irrelevant details: Is the mention of 8-flow at all relevant? I, at least, found the definition of L on the first line of the proof of Lemma 2.2 to be needlessly inscrutable, and my thesis advisor would have likely stopped reading there and told me to fix it.
Maybe someone should ask the model to make a more clearly written and thus easy to verify proof :)
I was confused at first when you asked if the 8-flow is relevant, when like, the 8-flow is a key input that the cycle double cover is built out of. Then I realized, oh, I guess technically they're not using the 8-flow, they're using the Z_2^3-flow. But like. The existence of an 8-flow and the existence of a Z_2^3-flow are equivalent, and I gather most graph theorists are going to talk about it in terms of the existence of an 8-flow, so noting that having a Z_2^3-flow is equivalent to having an 8-flow helps the reader to put this information in context.
I'm not sure why you find this proof so hard to read. I found it mostly quite readable (and the definition of L is straightforward? I wouldn't have written it quite that way but it's hardly inscrutable), although I feel like some parts are maybe lacking some exposition to explain the reason for certain things -- it doesn't feel written "in order". I also don't like that it's not cleanly separated into theorems and proofs -- some of the proof occurs in parts that aren't set off, for instance, and there isn't even a proper main theorem statement! But overall I was able to get through it without a lot of trouble and I'm not even a graph theorist...
My issues with the definition of L are mostly about the order in which things are written.
L(t, epsilon)_e breaks down the range of L onto its component values indexed by edge, but this only really makes sense when you know that t and epsilon are. They are sort of defined in the middle of a sentence in the proof of 2.1, which IMO is asking a lot of the reader, and this sort of sloppiness is a way that errors can hide in a proof. (Not that I see an error here. But a formalization in Lean or whatever would not get away with this.)
And, in the same definition of L, for some reason the e=uv part comes at the end only after u and v are used.
What would be wrong with stating, in the definition, what sorts of objects t and epsilon are and with omitting e entirely in favor of just calling the edge uv everywhere?
are the references real? how do you think it got access to those papers? were they somehow already in the training data, or a result of web searches, Google scholar, etc?
None of them include a web URL but in text some are super specific ("[3, Sections 2.1 and 3.1]" and "[8, p. 367]").
The references go back to 1954 (Chronologically sorted: 1954, 1973, 1975, 1976, 1978, 1979, 1981, 1985, 1987 and 1994.)
Since reference 10 is included as "personal correspondence" maybe the reference itself was copied from one of Tutte's other papers? Or how did it get that reference?
If it were a human (going off of memory as it has been a while), they would probably be using mathscinet and their university library to obtain copies of these papers online. Many old papers are digitized and available by these means. I’m sure the AI companies have it all easily accessible and/or the entirety of mathscinet is in the training data. The “personal correspondence” is possibly lifting from another paper or journal but yeah that is a bit odd that they wouldn’t source where they lifted that from directly.
I can’t say if the citations are accurate because I didn’t check.
Yes, reference 10 jumped out at me as well. I thought personal correspondence references typically include one of the authors of the paper.
It's definitely cribbing from other papers.
https://scholar.google.com/scholar?q=W.T.%20Tutte%2C%20Perso....
Sloppy scholarship. On the other hand, it's simply a credit attribution of posing the problem, so it's not material in evaluating the results. I observe that the majority of references I can find that attribute this to Tutte are very indirect - i.e., citing sources that themselves claim Tutte was one of the people who formulated it - so it would take someone with a little more time on their hands (or perhaps an LLM) to track down the original...
Over on r/math, one objection to the proof has been raised (more discussion is needed to know if it is a problem): https://old.reddit.com/r/math/comments/1uszk3d/openai_claims...
No, that's not a problem at all. It just the notation that's a bit weird.
For example, if e is the a-edge (first edge) from the u side and v is the b-edge (second edge) from the v side then g_{u,e} = 0, g_{v,e} = a so d_e = 0 + f(x2) where f(x2) is the flow (from Kilpatrick and Jaeger's NZ8F) on the first edge next to v.
I checked the whole thing with some surface reformulations on my side and it looks right to me.
That's a much shorter and more elegant proof than I was expecting, especially after reading some of the earlier Erdos proofs. GPT 5.6 Sol is the real deal.
Is this the first LLM-solved problem famous enough to have been on https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_m...
No there was the planar unit distance problem
(Erdős problem 90)
It looks like it was only added to that page under the solved section _after_ an LLM solved it
I just had Sol Ultra read the proof and create a graph of it using Concludia (my side project) so you can explore it visually/graphically. I certainly don't understand it though so I have no idea if it's helpful. :)
https://concludia.org/graph/g_2ecb8083-52ec-3448-8c30-2f9bc7...
the cycle double cover conjecture was open for 50 years. GPT-5.6 solved it in an afternoon and then asked if there were any more like it.
My bet they run gpt over dataset of 10k unsolved conjectures, it happened this one was solvable.
Is there anyone more knowledgeable than me about proof checking software who could tell me how off the mark I am here?
Assuming you have decent proof checking software, is it possible that this solution was achieved by throwing GPT at the problem a couple hundred thousand times until it passed the proof checker?
As someone who's used proof checkers a fair amount, if you don't have some high level idea about the proof, it's an open problem, and the hard part isn't some extremely tedious finite case analysis, it's extremely unlikely you'll get anywhere by trying to mechanize by throwing stuff against the wall to get it to typecheck. When people talk about mathematics being a closed formal system as though this trivializes any creative component, what they're omitting is that in type theory like that used by Lean or Rocq, there are two kinds of terms (match statements proving dependent elimination and fixpoints that provide proof by induction) where there's no real way to infer the type from the term. i.e., there are cases where you have to get creative and try to prove something more general than what you actually care about in order to get the proof about the original case to go through. What does "more general" mean? It could mean anything... that's the problem. That's why it's usually advantageous to reformulate the problem in terms of a different abstraction and build on top of existing results, knowing a lot about the literature and the way these kinds of problems tend to be attacked, rather than just chuck random terms over to a proof assistant and hope for the best.
Well the key thing here is I’m not saying the LLM has no idea what it’s doing. But LLMs are prone to hallucinations which can really impact a string of interdependent logic like a proof. So I’m assuming it would respond with something that’s not complete nonsense to this proof most of the time. Where I’m skeptical is if this was a true one shot, or if they had to iterate and try multiple different prompts, or even the same prompt over and over again to reach a working solution.
So I’m just asking if the proof checking software is capable of evaluating this proof. Because if it is, that makes the brute force approach a lot more feasible as you reduce human review overhead significantly.
If it is, that would imply you could run the prompt through the LLM as many times as you want until you “strike gold” so to speak.
I absolutely think that with the rise of LLM generated theorems we need mechanization more than ever, yeah. But I felt that was already pretty important for human proofs, too, and people are just more amenable to the idea now that it doesn't take such heroic effort to formalize things.
As far as whether something like Lean could evaluate this proof: sure, if it were mechanized rigorously. But the amount of work that takes to do varies with both subject and complexity of result. In this case, from what other people are saying, the infrastructure for doing graph theory proofs like this isn't as built up as it is for some other areas of mathematics, so it might take a while.
I see. So you seem to lean towards it being unlikely they would be able to use lean to evaluate this proof in an automated way…
I'm honestly not familiar enough with how well-developed graph theory is in Lean to be able to say. The paper is mostly using pretty old results, so it's mostly a matter of whether that stuff has already been formalized or not. Like anything else in software (and Lean proofs are very much software) a lot of it's about infrastructure. It wasn't so long ago that no area of mathematics outside of type theory and formal verification was really built up enough to do "serious" math -- that's changed a lot within the last few years.
What I'm more saying is that we're a ways away from being able to straightforwardly go from an LLM having a paper proof to having that proof formalized in Lean in the general case. Not so much because it's hard for LLMs, more just because it's hard in general unless all that background work has already been done. As more and more of foundational mathematics gets mechanized, it will be easier and easier to check your work in Lean while you work on the proof. For example, AFAIK unit distance has already been mechanized (though the quality of the mechanization effort sounds not great, it still greatly increases our assurance in the proof's correctness).
"But LLMs are prone to hallucinations which can really impact a string of interdependent logic like a proof. So I’m assuming it would respond with something that’s not complete nonsense to this proof most of the time."
Unfortunately in my experience that's not really the case. For me, very often GPT 5.5 (which was a good deal better than Opus at this kind of task) would just get stuck for long periods when working in a logic like Iris. It wouldn't necessarily outright prove nonsense, but it would vastly overclaim what it had proved and failed to get anywhere without a lot of hinting. 5.6 is hopefully a lot better about this.
As someone who was a research assistant in this field one summer back in college, I spent the day trying to check the proof, or at least the obvious places a mistake would be. It's surprisingly readable, so I guess we'll find out soon.
Lemma 2.2 specifically "feels" new to me. You can get part of the way by duct-taping several papers together (playing along at home: I found Tutte 1954, Bermond–Jackson–Jaeger 1983, Máčajová–Škoviera 2005, Zaslavsky 1982. interestingly, only Tutte appears in the works cited). But it's surprising you'd think to pick those, and surprising it works, because you still need a genuinely novel parity argument at the end. Those steps individually are all pretty simple, knowing to chain that chain together, isn't.
The guess-against the checker paradigm is real (ie AlphaProof), and something like that was probably involved here. But this area of graph theory isn't in mathlib, you need to write the proof checker first, and then you need to know what kind of proof checker you need to write (or just do a brute force search for new proof checkers). Probably how you got this result is have a recursive tree of agents until you divide into small enough subproblems.
At a certain point you need a philosopher to figure out what that "means", ie if you have a big enough tree of small enough subproblems, some of the "magic" so to speak moves out of the proof checkers and into the way the tree got structured.
On the last Dwarkesh podcast with 3blue1brown, one of them mentioned that frontier models are now able to work through a whole proof in natural language, just like a human mathematician would. But when they first solved IMO problems in 2024, they relied more on Lean to catch hallucinations.
I don't have the $$$ to throw at this, but it would be interesting to see how other models tackle this.
Would, say, Fable or GLM 5.2 solve this given infinite amount of time?
Statement of AI use. The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex (with GPT 5.6 Sol).
Clearly that sentence isn't AI generated ...
What was the prompt that was used to generate the prompt?
How many cycles did it take to cover all the bases twice?
OpenAI knocked it out of the park with this one.
Has it been audited and verified?
Next question: what future inventions can be accomplished with this?
what's the difference between Sol Ultra and Sol pro? is pro a thing of the past now
Ultra = parallel subagents with max reasoning
Pro = test-time compute (best of N responses)
Confused about how to access Ultra; I don't see it in on their plans page.
Ah, I see it as a "reasoning level" in codex after typing /model
why would you use one over the other?
> GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture
Very misleading article title.
Title should be "Un-named humans produce unverified proof of CDC Conjecture using GPT-5.6" ... but I expect only advertising copy when it comes from the AI industry.
It's been amusing to watch the points bounce up and down on my comment.
I guess equally half the readers agree with my sentiment, and half down-vote, being upset by my attitude to the AI industry :)
PS. I'm quietly waiting for the bubble to pop - the main interest being will it pop with a bang and cause grief to many, or will it just go with a long drawn-out fart that can be ignored by most.
chip production and network acceleration here we come
This is not a remark about AI, but there's something funny about mathematics in that every novel result is broadly perceived as a big deal.
We attach basically zero value to writing a new program that hasn't existed before, or a piece of text that hasn't existed before. It's boring, or even a net negative, unless you can show that the result benefits the world in some way. We'd find it weird if OpenAI put out a release saying that an LLM authored an interesting blog post.
For mathematics, I think it's really a matter of two things. First, the generation of proof was so severely resource-constrained on the human end that they could actually afford to celebrate every contribution - akin to how software engineering would look like if you had just 200 active SWEs in the entire world. But compounding that, mathematics is basically the only scientific discipline that rejected any notion of utility. It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
> rejected any notion of utility. It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
I disagree. Mathematicians care about the utility of a result. It is just that they regard mathematical understanding as a valid type of utility, and that can be arbitrarily far removed from practical utility. But a proof that doesn't help anyone understand anything interesting is not valued. I could go out and define some pointless construction and create proofs about it immediately. It would only matter if I connect it to some other subject of interest within math.
I would argue that mathematical understanding is valuable for extrinsic reasons, but it is true that by the time you're a math grad student, you're usually willing to pursue it for no external purpose.
Although not a mathematician, Daniel Dennett had a wonderful example about higher order truths of "chmess". https://personal.lse.ac.uk/robert49/teaching/ph445/notes/den...
> and that can be arbitrarily far removed from practical utility
In which case it’s ~equivalent to not caring about utility
It seems in mathematics that the utility of a problem is directly correlated with how difficult it is to solve, for some odd reason. If I defined some pointless construction and it turned out to be very difficult to prove, it would automatically over time become considered a "high utility" mathematics problem (again, for some odd reason).
Mathematics is largely just smart people working on pointless puzzles, and only by coincidence do these puzzles turn out to have practical applications (it cannot be predicted). Or I guess all the obviously practical problems in mathematics have already been solved -- we're now in a world where math is rarely the limiting factor for human progress (like it was, say, pre-calculus; was FFT the last significant unblock from math?).
It's such a waste of the best human minds. Or maybe the best human minds are actually doing something else, maybe we only notice the handful of Terence Taos, not the hundreds of people of equal brilliance who realized pure math is pointless and decided to pursue physics, rocketry, or quantitative finance.
> If I defined some pointless construction and it turned out to be very difficult to prove, it would absolutely and automatically over time be considered a "high utility" problem (again, for some odd reason).
Yes and no.
No: There are lots of very hard open problems which are judged to be of little value by mathematicians and hence garner little attention.
Yes: If a conjecture resists proof for a long time, this can indicate that we still have a substantial gap in our understanding. We project utility into an eventual closure of this gap, not into the statement of the concrete conjecture at hand. The gain in understanding is what we actually work for. It just turns out that chasing specific results, even if they are mostly dead ends on their own, is useful for orientation.
The (by now solved) problem by Fermat (for all integers a ≥ 1, b ≥ 1, c ≥ 1, n ≥ 3, the equation aⁿ + bⁿ = cⁿ does not hold) and the (still open) Collatz conjecture are perhaps good illustrations of this situation.
Writing that mathematics is a waste is such a hilariously ignorant comment to make on a programming forum.
remarkable also how it's not even greyed out either. I have been downvoted to oblivion for far more defensible claims
Your comment is somewhat emotionally charged, but I choose to respond to the overall point as a mathematician. I think it could be true that utility is correlated with difficulty but it is certainly not defined by it.
In pure mathematics, we reason about a world of abstract objects which are considered interesting ab initio. It may be because they arise directly or often from extremely basic operations, they are connected to many other interesting objects, or that they present special and surprising properties. The importance is basically, there is some surprising, interesting, phenomena which occurs in our world which we don't understand and which we seek to understand. Like science but in the non-physical world.
I think if you create a simple to describe system/construction with a property which is extremely difficult to prove. You are creating an object in our world which is basic but have properties which we don't understand (because we can't prove this property). So indeed I believe it would be an interesting thing to study and be of value. I don't see any problems/issues with this. I don't think the only valuable pursuit of humans is to improve the welfare of other humans. I think understanding the world is also valuable.
Most fields, in the aggregate, produce a lot of pointless work, but if you judge mathematics by its best examples, as judged by the field itself, and also by the outside intellectual community, it is a coherent body of work (& brilliantly creative). It is not pointless puzzles at all. William Thurston's geometrization theorem, Klein's erlangen program, Witten's work in physics-inspired mathematics, Langlands program, the Grothendieck school of Algebraic Geometry are deep and abiding intellectual achievements of true understanding. If you don't understand the meaning behind this work, it speaks to your ignorance, not to their significance. The "obvious practical problems" are not solved. Fluid Dynamics is wide open. Non-perturbative quantum theories are wide open. Heck, there are open mathematical problems in General Relativity. Dynamical systems are very poorly understood. Go read a book or something.
There was no useful math after 1964? What? Or do you not count the entire field of computer science as math (arguably FFT belongs to computer science too)?
>mathematics is basically the only scientific discipline that rejected any notion of utility
I think this might depend on the department, but I was at a pure math department last year, and struggling with my Linear Algebra textbook (written by the professor, incidentally, who was not a great communicator).
I consulted the machines, and learned, to my great delight, that linear algebra is used in like 20 different fields in the real world. It's "perhaps the most applied branch of mathematics in existence".
I complained in the group chat, that our didactic materials, specifically tasked with providing motivation and concrete examples, did not contain a single application, of this most richly applied field.
I was promptly pilloried, and shunned.
(Apparently that particular department was the wrong one, to ask a question like that!)
I’m a physicist, so I’m biased, but my experience of pure maths was about the same. We had to do it, but at no point was any utility actually demonstrated - that was left to the physics professors. It was all just “look at this thing I can do with these symbols” without any actual tangible relationship to anything.
Then again, I remember how we were taught calculus at high school - we were taught how to mechanistically integrate and derive everything under the sun. At no point did anyone think to explain that we were measuring the areas under curves, or their rates of change - it was all just “memorise this operation”. Again it was left to the physics teachers to explain why this was useful, and what we were actually doing.
Poor teaching, if you ask me, and it more often than not left me retrospectively wondering if said mathematicians had actually understood any of what they did, or if they just had little blind symbol manipulation Turing machines in their heads.
Re: obvious intuitive explanations are ignored.
I remember squinting at the definitions in my calculus textbook for a full 10 minutes before realizing... oh my God, if this had been a 5 second animation, I would have understood it instantly.
I remember being rather upset! "If it's so obvious and intuitive, why didn't they just say so?"
I want to say, "well, unfortunately you cannot put an animation in a textbook." But that's actually false!
Even as a child I made flip book animations. And there was plenty of room here in the margins for several of those :)
Teaching only the practical side risks not teaching the subject with the appropriate theoretical depth and the ability to generalize it to other applications. Courses for purely applied fields utilize calculus to solve the current problem and then move on without teaching the finer points. Basing a calculus course on physics alone might be preferable in high school, but would be of disservice to students in university.
>At no point did anyone think to explain that we were measuring the areas under curves, or their rates of change
In my experience you get taught the definition of a derivative of a function at a point is equal to the instantaneous rate of change and that integrals are defined as a Reimann Sum, the sum of the area under the curve. Everything in the class comes from building on top of those definitions.
That you think this way (and if like me, it makes you excited!) I think it's because it has clicked for you.
For many that light bulb above their head doesn't flash on, hence they get to dislike the subject or forget it after they are done with their studies. I was lucky enough to appreciate math that much to redo it in my free time after high-school and make it click for me.
No, my calculus class in HS very literally started with finding the area under a curve “manually” and introduced integration as a generalization of that. I’m not surprised to hear that calculus is sometimes taught very poorly, but it’s not universal.
Well, in at least some cases, they do understand what they're doing, on a deep intuitive level!
Using spaced repetition to see through a piece of mathematics
https://news.ycombinator.com/item?id=18895613
The title is a slight misnomer in my opinion. The author did make heavy use of spaced repetition of course, but deemed it neither necessary nor sufficient for the result he described.
The actual active ingredient is curiosity to the degree of obsession. Actually wanting to understand what's going on.
You can do that with pure math just as much as with applied.
But it may be harder for many people for such a desire to arise if there is no obvious connection to real-world matters. (I certainly had such thoughts, sometimes! What is this for? What's the point?)
> I complained in the group chat, that our didactic materials, specifically tasked with providing motivation and concrete examples, did not contain a single application, of this most richly applied field.
> I was promptly pilloried, and shunned.
Heh. In my day I may have participated in the pillorying.
I do think that there is value/merit in professors mentioning real world applications, where they exist.
What they're sensitive about are the theorems where there aren't real world applications. They don't want to (and shouldn't) justify them.
So even when there are real world applications, the posture is "Who knows if someone is making good use of this in the world somewhere? I don't care. It's not why we learn or teach this!"
Knowledge for its own sake is great, but it's worth noting that many "useless" fields of mathematics turned out to be very practical in the long run.
Number theory was long thought to have no practical application, but now it's the backbone of cryptography. Boolean algebra was developed in the 19th century (George Boole died in 1864), decades before it was used to build computers.
Those "useless" theorems being proved today may turn out to unlock a world-changing technology centuries from now. When the breakthrough comes we'll be grateful for the people who laid the foundations.
No one is disputing that - not even most mathematicians. They just don't want it to be their job to know the useful applications.
Hear me out on this one:
For a lot of math departments, that is exactly why they teach this. Education is rooted in application. We have entire careers that depend on certain aspects of mathematics, so most companies gatekeep that career by a degree. The degree requires the class. The student taking the class may not even be old enough to drink alcohol yet, and they can't possibly be expected to know of all the applications. Knowing and not telling them is doing them a disservice.
> For a lot of math departments, that is exactly why they teach this.
Depends on the course. That's why some departments have separate calculus courses for math majors - because otherwise the whole class will be full of non-math majors (engineers, etc) and focusing on their needs does a disservice to the students in their own department.
> The degree requires the class. The student taking the class may not even be old enough to drink alcohol yet, and they can't possibly be expected to know of all the applications.
If I'm a CS major, and the degree is requiring a class outside of the CS department, you shouldn't expect the professor of the class to know why the CS department is requiring it. It's on the CS department and its faculty to explain it.
The ultimate goal of university education is to raise researchers, who are the people that investigate the knowledge frontier of their field and then advancing it. To do that they have to understand a large part of the existing field so they can communicate with their peers, avoid investigating things that have already been throroughly explored, and draw useful connections to other fields.
Even in more applied fields it can take decades before advances become practically relevant. Restricting teaching to topics that have immediate practical relevance would therefore do students a huge disservice and prevent them from approaching the knowledge frontier of the field.
> The ultimate goal of university education is to raise researchers
The head of my CS department was quoted as saying, "our job is to produce researchers!"
This was in the context of a conversation about why the program wasn't better suited for industry.
It turned out that in our department 7% of students ended up going into research.
So he was openly declaring his intention to disregard the needs of 93% of his students.
(I'm not arguing against research, or on going deep with the theory. I just thought that was kind of funny, and it seemed a bit wrong to me.)
CS is special in that it is about the science, and not the application. They'll teach you mostly theory. That's why some universities/countries have a separate degree called "SW Engineering".
Other engineering departments are not as fussy about the distinction.
I think for many people (myself included) understanding mathematics is rooted in application because it helps bridge the divide between intuition and rote memorization. Without the application, IMO instructors are doing a disservice to their students and pedagogy of mathematics itself. They’re intentionally ignoring a significant fraction of the class, unless they’re teaching some esoteric grad level pure math.
Yeah this was my position. I don't mean "Sally has six apples" necessarily, but my brain needs some concrete handles to grab onto so it can actually manipulate this stuff intuitively.
See also: Using spaced repetition to see through a piece of mathematics
https://news.ycombinator.com/item?id=18895613
Where the author describes his mind eventually turning the mathematical objects (symbols) into some kind of mental objects he was able to actually manipulate "directly". As a result of this facility, his mind spontaneously produced many new insights into the matter.
That level of fluency obviously requires a great deal of work, but in my experience it can be approximated and accelerated with analogies. (e.g. see Feynman's teaching.)
I love teaching kids and young adults calculus by socratic method. They get so mad when they figure out you were teaching them math, but they often admit it was pretty fun. Only had the chance to teach like that a few times but it's dynamite when it happens.
I did this when I taught my third grader calculus on the train, when she asked a question about the train accelerating faster sometimes than other times. She loved it, but I was just taking advantage of children's natural curiosity.
Do you have some examples that the adult could instigate, rather than waiting for the child to express curiosity?
I've used filling a tank, balloon, or bucket (rate of flow, can be subdivided to teach limits, and use weird shapes for teaching area under curve and interpolation en route to integrals), or the classic throwing a ball back and forth and trying to describe the shape, the distance it flies, peak speed vs peak height, figuring out how hard you are "actually" throwing instantaneously. Honestly as soon as you start thinking about bulk substances moving around (gravel piles! fuel tanks!) it's easier to find examples than you'd ever reckon. Rate of change is everywhere.
Seems like I start by asking "how do we know how much this tank holds?", or "how fast does this line go up on the side of the tank?" and curiosity goes from there usually.
Yes, exactly, identifying things that change is the key. Thank you!
I thought linear algebra was pretty much the poster child of applied mathematics - the entire field was invented to represent computations in a regularized form to feed into computers. Well not really, but much like Boolean algebra or the Fourier Transform, it was pretty much a curiosity until computers came along.
> but much like Boolean algebra or the Fourier Transform, it was pretty much a curiosity until computers came along.
https://en.wikipedia.org/wiki/Linear_algebra#History: “Later, Gauss further described the method of elimination, which was initially listed as an advancement in geodesy”
That’s an application of linear algebra in the 19th century.
Many important advances in linear algebra happened in WWI to solve optimization problems for logistical and industrial planning. A lot of these applications boil down to high-dimensional systems of linear equations, which back then were solved by hand. Efficient algorithms translate to reduced labor costs.
>(Apparently that particular department was the wrong one, to ask a question like that!)
Yes, the math department.
In any case linear algebra, stochastics, calculus; plenty of engineering and science applications for all these.
despite being theoretical i would have greatly benefitted in learning linear algebra if i had seen even one or two not-obvious applications, like galois fields for reid solomon erasure coding.
As my Linear Algebra prof used to say, basically everything is applied Linear Algebra.
Even when this really isn't the case, the math is preferably reduced to a linear problem whenever possible since dealing with the original complexity is usually so much more painful.
As a friend of mine who also happens to be a math professor once said: mathematicians are like sculptors who marvel about the beauty of their creation, and are kind of disgusted when a physicist comes nearby and says “that's a cool hammer you got there, may I borrow it?”.
I would be flattered , but that is just me
John: "I've just gotten word. They found an application for my theorem. They say they've used it to cure cancer."
Frank: "I'm so sorry."
If it was the students, then students can have things they think are cool or uncool.
If it was the professor, then that would be very embarassing on his or her part.
Typical pure-math linear algebra course has to cover so much material that there's really no time for applications! That's why applied math is typically separate track.
Biologists celebrate the discovery of new species of fruit fly hidden deep in the Amazon rainforest. Astronomers celebrate the discovery of new giant rocks located zillions of light years away. Neither of these things is immediately “useful” to the world, although they may turn out to be enormously beneficial in ways we can’t immediately predict. To me, these fields also feel central to the human experience—discovering new types of life, or learning more about our place in the universe. I don’t think a mathematical proof is any different.
> This is not a remark about AI, but there's something funny about mathematics in that every novel result is broadly perceived as a big deal.
This isn't true using the level of originality you're implying with your software examples.
Technically speaking, many novel mathematics proofs are written all the time (quite a few textbook exercises are actually technically novel problems that have never been posed before they were written in a textbook!) that get absolutely no fanfare. Overwhelmingly though they are not very original or difficult and really just required a fairly routine combination of different pre-existing techniques, even if technically speaking that combination didn't exist before. Those textbook problems are hence easy and therefore not given much public attention even if they are technically novel problems.
Indeed over the course of developing a new mathematical result, many many novel results are glossed over to the extent that even their proofs are left out ("as an exercise for the reader") because they are fairly trivial.
This is true for the overwhelming majority of new software as well. A new CRUD program may, technically speaking, be novel, but it's almost certainly just a routine combination of different pre-existing things.
Mathematics open problems that are actually named are generally problems that have resisted the low hanging fruit of the most obvious combinations of pre-existing problems. When those are solved they are a big deal precisely because they usually require some novelty!
Similarly in software, if someone were to create a new kind of database that solves a variety of new classes of problems that current databases fail to solve that would be a big deal! Truly novel software is also perceived as a big deal. Software that is, technically speaking new, but doesn't actually stray far from a fairly obvious remix of pre-existing techniques, isn't really celebrated.
In both software and mathematics, the intuitive benchmark is if other practitioners in the field look at the result and would say "Wow! How did you do that?" Professional software developers generally don't look at, e.g. a new blogging platform, and boggle at "Wow! How did they make that?!!"
I'm not a mathematician, but I don't think that's true..? It's just that some problems are considered "hard" or known to have been "open" for a long time or that involve some clever/pioneering new technique. There's tons of math papers out there that are in some technical sense a novel contribution but in practice just languish without much attention except maybe from like two other people working in the same subfield.
This feels mistaken; we develop abstract objects i.e. graphs based on real-world utility or whatever. As we try to improve our understanding of graphs, we value proofs that help us do so, or help other fields of mathematics. We assign 0 value to random proofs about stuff no one cares about... This conjecture had value, simply because some people found it interesting. It is not really different from music, in a sense.
> It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
No, the value is that Erdos's name is attached to it.
Lots of mathematicians prove things they don't publish, or their manuscripts get rejected - not because of a flaw in the proof but because no one cares about the theorem they proved.
And I'm sure it'll be the case with LLM models performing proofs. It'll be notable only when the theorem is a known one that people have had difficulty proving.
> No, the value is that Erdos's name is attached to it.
That's unnecessarily reductive. you could have said "most of the value is that erdos' name is attached to it"
It’s far from a perfect analogy but I would imagine that people were pretty hyped about the novelty of the first legitimately useful compiled programs where they didn’t have to allocate their own registers. I wonder how long it took for that novelty to wear off?
Or in other words I’d argue novelty is contextual and that these kinds of discoveries’ novelty will eventually wear off too but for right now it’s pretty cool that the “math discovery compiler” works well enough to do this (again imperfect analogy).
Wow, you couldn't be more wrong here.
Math is something humans invented and is a model, nothing else. There is no logic per se, but a model that works quite well for us.
I studied Math and CS as a very highly gifted and quickly found out, there is no beauty of Mathematical Logic, only humans approval of what they deem most accurate.
A good example is set theory. Cantor was not openly welcomed after he introduced his "theory" to others. In fact, he was received quite some pushback and hostility - this doesn't sound like someone received love the mathematical logic's way.
In fact, the story of Cantor is really a tragic one. He left math for quite some time, due to the pushback.
Only later humans accepted his theory and found it useful. Well, well, what is Mathematical Logic and what not is after all just broad consensus by humans.
And if you go deeper, you will hear more of these stories. Math is anything else but logic. Proofs are religious things, often so complicated, they are simply accepted as "approved by a committee". Many profs cannot really explain simple proofs, they refer to the textbook.
This doesn't sound like romance nor easily reproducible logic.
After all, we deal with human beings.
You're also wrong
"Math is something humans invented"
Majority of mathematicians are platonists and believe arithmetic was existed and was discovered and was not "invented".
"There is no logic per se"
There is logic to it! Most logicians are mathematicians at heart. See Russel, Godel, Hilbert, etc
"no beauty of Mathematical Logic"
Mathematicians do focus on beauty. Entire books have been written on this. G.H. Hardy in A Mathematician's Apology even said math MUST be beautfiul
"Proofs are religious things"
What are you going on about...
Consensus may give a hint to what is or isn't reality. But consensus—even expert consensus—does not determine reality. Experts can be wrong. Most of the experts, even, can be wrong simultaneously.
Philosophy is the exercise of testing ideas for oneself in the laboratory of one's own mind.
When I test the idea that math is discovered in my own mind, from my own perspective, with my own experience and education brought to bear, I find it unconvincing.
When you test the same idea in the laboratory of your mind, with your experience and your education applied, and get a different result, that is interesting. Your result is relevant information to me. If nothing else, it's a good prompt/trigger for me to revisit my earlier conclusion and see if it still holds.
But your disagreement—or indeed, the disagreement of a majority of trained mathematicians—does not constitute an automatic reason for me to conclusively determine that you/they are right and I am wrong.
I still have my own examination of the concept, with my own supporting and detracting arguments. And the result of my examination continues to be that math being invented is the significantly more persuasive view.
No matter what humans do, it somehow ends up being a popularity contest.
It's almost like a twisted mirror of Conway's law.
> We attach basically zero value to writing a new program
What does it mean "new"? And, was it a difficult or trivial accomplishment?
A solution to a well known open math problem is both new and non-trivial- you know that many, very smart, very well trained human experts have dedicated time to the problem and haven't been able to solve it, despite good incentives.
[dead]
There is a tension between applied and theoretical mathematics, and it's as old as the whole science itself. Mathematics arose to solve practical problems (land surveying and division, as well as trade) and recognizing the underlying principles make it possible to abstract that knowledge. That might lead to centuries of ivory tower activity and what could be regarded as a purely artistic pursuit until somebody figures out how to apply a theory to a new practical problem. Or relations to another theory are discovered, and suddenly there is a new approach to previously intractable questions. A good example is be number theory, which is the foundation of modern cryptography.
> there's something funny about mathematics in that every novel result is broadly perceived as a big deal.
Is this true? Or is it just that mathematics is an isolated enough field that only the results that are a big deal get broadcast widely to the public.
I know little of the inner workings of the field of mathematics, but my naive assumption would be that there's probably lots of novel but boring results being discovered/proven all the time and we don't hear about them because no-one outside of the person doing the work and a handful of their colleagues is really that interested in it. Likely a lot aren't published in any way, because they're just stepping stones towards the goal of the actual area/paper/whatever being worked on.
The reason novelty matters for mathematics is that they strictly deduplicate all claims. If someone claim they proved something that we already knew was solved, than that wouldn't be considered novelty. Novelty and deduplication is the combo here. This is not true for blog posts.
The difference is discovering or proving a universal truth that will go into the corpus of human knowledge forever versus some app to shuttle money around or help people count how long they’re sleeping. It has gravitas unlike some nifty super performant text editor.
> We attach basically zero value to writing a new program that hasn't existed before
We don't? People write new programs that go on to be successful software companies that make millions of dollars! Basic CRUD apps make money for their creators in their niche! There's so much money in software that it's taking over the world. The market is different, you're not getting worldwide household recognition for every little fart or sneeze of programming you output, but how can you say that we attach zero value to new programs when the history of computers is insanely valuable companies making new software and selling it. Windows, Oracle, mongoDB, etc.
> It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture..
I'm not sure about this, TBH I ask myself this quite frequently. In a world where machines are routinely solving very high end math problems every day, producing more proofs than humans would ever really be able to absorb or fully understand.... would that be a good thing? Would that in itself be valueable? It feels like that is a probable future, but I'm not sure that would actually be something we want. I think there's probably more than "value is that it's solved"
Isn't it immediately obvious that solving something that humans have been unable to do for decades or more is the most tangible proof of ASI, or at the very least pretty good AGI?
Is this something humans have been unable to do?
There’s only so many people with the necessary skills to solve this. And you need these humans to choose to spend their time solving this, and not something else.
>Is this something humans have been unable to do?
It's a famous open problem so yeah
>There’s only so many people with the necessary skills to solve this. And you need these humans to choose to spend their time solving this, and not something else.
Sure, but that doesn't mean a lot of very skilled people hadn't attempted and failed to solve this.
And you’ve known about this problem for how many minutes?
Long enough to know this has been on the Wikipedia page of open math problems for several years.
A lot of mathematics often takes 100+ years to find a practical use because we have developed it so much that we have use all the easy maths. Things like CS or SWE are so new that you can still find stuff today that can be used tomorrow. Things like computation and cryptography was all discovered like 100 years before we had a practical use for it. Its an example of late stage scientific discipline. Things like physics, chemistry and biology will get here as well eventually.
It's newsworthy because it's a milestone. It was something no human was able to do (despite trying very hard), but a machine did. Humans have written lots of interesting blog posts.
The idea that mathematics has rejected any notion of utility is absurd. It's not like topics get picked at random. Conjectures like this are interesting because they are a test of our understanding. The problem sounds easy, but apparently was quite hard.
Mathematics isn't a scientific discipline.
> It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
I suspect the value is in showing the potential that LLMs have in developing new breakthroughs.
there is no "software" that a lot of people want, yet nobody managed to create yet because they failed too due to it was being hard to implement (excluding AGI/ASI which is not really software)
As a person who has a number of relatively niche hobbies, I assure you that this is not true. There's a ton of simple things that can be build and will make an immediate difference in the lives of thousands. Watch the workflow any musician, videographer, machinist, etc - they're full of small, weird inefficiencies that AI hasn't really solved for them.
It's just that you can't build a billion-dollar company around it. No one could go to a VC and say "we're going to be the Uber of focus stacking and dust removal for microscopy" or "we're the Uber of aligning the beats in two audio tracks".
> there is no "software" that a lot of people want, yet nobody managed to create yet because they failed too due to it was being hard to implement (excluding AGI/ASI which is not really software)
What!? I can think of about a billion examples... but for one, I'm still waiting for a good enough CFD/FEM coupled system to model paraglider dynamics across collapse/recovery. And I expect to be waiting quite a while.
5 minutes of wikipedia search would give you plenty examples of complicated software engineering problems that would have a big impact on everyone's life.
This is not true.
What is the perfect video game that makes the user infinitely happy?
What is the perfect economy optimizing program?
What algorithm can solve political strife?
As with all things, the answer is always "it depends" based on what is being optimized
In math, the utility lies in the proof itself. A novel proof of a hard problem usually comes with new insights and abstractions that help solve even more mathematical problems.
To go with your analogy, mathematicians care more about the source code of the program than about the result of the program. But I'm afraid that we will see things change with the increase of vibecoded proof slop. A black box proof is not as useful, even if it is correct.
Mathematics is what everything else is built upon. I'm no mathematician but a very good friend of mine is: teacher at a big uni, researcher. Pure math.
His entire life he's had --and still has-- to deal with comments like the one you just made, implying that the only value is solving pointless conjecture (if it wasn't pointless, according to your logic, then the value wouldn't be that it is solved).
Truth is to be found in this xkcd:
https://xkcd.com/435/
"every novel result is broadly perceived as a big deal" is not at all true. AI companies hype any novel result as proof that AI is good for mathematics, but professional mathematicians write tens of thousands of papers every year, and for 99.99% of them, nobody cares or writes it up. Mathematicians certainly don't go around saying each and every novel proof in their papers are a big deal. Do you have any evidence supporting your statement that it is "broadly perceived" (by whom?) as a big deal?
Sorry but I completely disagree with your statement that "every novel result is broadly perceived as a big deal". Most results certainly are not consider this way (even though the average result has difficulties that are much higher than novel computer program you may have in mind -- no offense)
I mean, OpenAI delayed the public release of GPT-2 back in 2019 because it seemed capable of authoring interesting blog posts (that also happened to be untrue). It was a pretty big deal the first time Transformer models were capable of generating that kind of output--no one found it weird. We've just grown to take it for granted that large Transformer models are this capable.
The same cycle is happening now for a harder frontier. And proofs represent a pretty good benchmark for model capabilities, so a new model proving a result that a previous model didn't is generally notable in the same way that a model scoring higher on a benchmark is.
I'm sure we'll take it for granted in the not-too-distant future.
Proving a novel math theroem now is incredibly hard because all the easy ones have already been proven.
We generally do give a lot of credit to programs that do something novel. The first gets a lot of credit. But if its just another CRUD app, nobody cares.
Its the same with proofs. First time someone proves something gets a lot of credit. The second proof for the same theorem gets a lot less buzz.
But even then, math proofs mostly get buzz when its something famous or at least important. Proving a random lemma usually doesn't get much buzz.
So I suppose the value is that something like this gets used as a primitive to solve something that actually has impact. Ah, mathematics, never change!
[dead]
It did not use Lean or other proof assistant?
There's really no good proof system mature enough to do advanced graph theory. The leading library in Lean is Graphlib, and it's really not ready for research level theorems.
How many tokens would it cost to write some library functions to fill in the gaps?
You could try solving that in Lean perhaps
what kinds of proofs would it be good at? I thought that combinatorial proofs would be easier to reason over than ones that required analysis
Graphlib? Do you have a link to this for me?
I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean
But is the proof accepted to be correct? That is what distinguishes this from being notable compared to any other AI slop proof.
Yeah it's a very very short proof that uses no mathematics developed within the last 30 years. Which doesn't necessarily make it wrong, but in the absence of mechanization in Lean or proper peer review I think this it is premature to post this. Notably the unit distance proof did not fall into this category.
I'd guess that verdict (or its opposite) is to come within the next 24 hours.
I would assume/hope they had someone verify it before publishing
Let me stand here on the Skeptic's Corner and be skeptical, so that the users who complain about skeptical comments have someone to direct their ire at. You're welcome.
Right, so, first, I haven't looked at the proof. Graph theory is not my subject and it would probably take me a few days to get my head around the whole thing. If OpenAI's LLM was used to prove an important graph theory result, then that's very good for them and graph theory.
However, I have to note that it's been 52 days since 20 May, the last date that OpenAI announced their previous mathematical result (a disproof of the unit distance conjecture).
What have OpenAI been doing all this time? I am willing to bet a good percentage of my money that they were trying, and failing, to produce the current result, or possibly something even juicier (one of the Millenium prize problems maybe?). They are hell bent on showing that their models are good for maths and science so they're very unlikely to have sat there twiddling their thumbs until they suddenly sprang into action and prompted their LLM once to generate just one proof. They must have been running the thing constantly, multiple instances of it, over that entire period.
Going by the instruction to run for eight hours before returning or giving up in their released prompt [1], that means they could have made at most 156 attempts to solve this problem, each of which failed except the last one [2].
So what happened to those other 156 attempts? Are we ever going to see them?
More importantly, who was it that selected the announced result? Who decided that this result is an actual proof? Until now, every proof generated by an LLM has been verified either by human mathematicians, or by human mathematicians x a proof assistant. What happened this time?
Obviously, any claims that this result were produced "autonomously" must be evaluated according to the answer to that last question. So far, LLMs have been incapable of distinguishing between a correct and an incorrect proof, which is also why they need to be run multiple times until they generate a correct one. If something has changed, it'd be interesting to know.
Finally, a magic eight ball that's correct one time out of 156 may be useful; or it may not. I honestly have no idea. I think time will tell.
__________________
[1] "Spend at least 8 hours on this before even thinking of returning or giving up"
https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...
[2] That's 52 days from 20 May, times 3 for each eight-hour attempt in a 24-hour day.
But note well that the X post says that the solution was produced in "just under one hour" so that means the model didn't really stick to the prompt's time limit. Which means there may have been considerably more than 156 attempts that we'll probably never know of.
Or even considerably more if the model ignored the time limit going the other way.
Since this isn't in Lean and it's extremely easy for something like this to contain a subtle mistake, I think I'd prefer this be announced by a professional mathematician. The proof appears relatively short and elementary (not to be confused with easy -- just not using any advanced or modern machinery) so it shouldn't take long for the mathematics community to do a peer review. Without that, you could easily crank out hundreds or thousands of PDFs like this that all look plausible and are beyond the ability of a gifted amateur to review.
https://github.com/openai/cdc-lean
Perfect -- that's great to see. The proof strategy in Lean appears essentially identical to the natural language strategy (as much as is reasonably possible). I think this settles it!
But they used LateX
…and thank God it's not Lean.
Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.
Human unreadable proofs have only limited value.
I disagree. It's the only way to scale AI mathematics far beyond human mathematics. Any interesting verified result would, obviously, be rewritten back into natural language for human understanding and consumption (as well as potentially for the benefit of AI conjecturers too). You are falsely assuming that advances in formal mathematics would not feed back into similar (potentially massive) advances into informal mathematics, and I think that's simply wrong. We're just at the very, very beginning of that curve.
I think this is, in fact, inevitable. It's the exact same RL loop that allowed AlphaGo to vastly exceed the world's top human players. You can theoretically RL formal proof techniques vastly beyond human capability by removing the need for any human review for correctness. It is completely reasonable to assume that "informalization" will become a real sub-field of mathematics in the near future.
I didn't say they have no value. Just limited value. A novel readable proof that expands the horizons of human insight is certainly more valuable than a megabyte sized trychnobezoar of machine generated predicates.
You are assuming that the latter, once autonomously discovered and verified at scale, could not simply be translated into the former, also perhaps autonomously at scale (or otherwise selectively as determined by human interest, taste, and relevance).
Well we're literally discussing a human readable machine generated proof here yet you don't seem happy with that.
We're talking past each other for some reason. I'm not "unhappy" with anything. I just pointed out that (1) a result like this requires peer review by a professional human mathematician, which fundamentally bottlenecks progress in a pretty severe way; (2) such review would not be necessary if it were accompanied by a formal Lean artifact; (3) you can have both a formal proof and an informal proof together (one does not rule out the other); (4) searching for proofs formally first, then translating successful auto-verified proofs into natural language, is the most scalable approach in the near future for AI mathematics; (5) AI conjecturers would likely benefit from the results of (4) for making large leaps and connections, which can then scale into formal proofs for verification, which then feed back into the same loop ...; (6) humans guide this process through taste, judgment, and their own intuition, likely often intervening to ensure that the loop is aligned and producing a body of conceptual informal mathematics that is valuable to humanity.
Why not both? Not sure why you're presenting this as one or the other.
What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.
If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever.
How does it matter if it Lean verified or a human verified proof if you comprehend neither?
There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.
One requires you to trust a human and the other requires you to trust mathematics.
Let me simplify it for the sake of argument. Imagine I am unable to follow a middle school proof of Pythagoras. How does it matter if I trust anyone beyond that? What possible contribution can I build on top of that?
It's great that a novel math proof was created.
But this is mostly marketing, pleasing the sneering class/the elites who believe that simply providing value for others (through sales) is repugnant and beneath them.
It seems that these tools can do real work, and people are paying for that. IMO, that is more than sufficient.
No one here actually cares about Cycle Double Cover Conjecture. I can demonstrate this by pointing out that the only time this conjecture was ever mentioned on the website was 14 years ago in a submission[1] that linked to a (now retracted) proof paper. That story received exactly zero upvotes. No one cared enough to upvote it and no one cared enough to ever mention this conjecture again.
[1] https://news.ycombinator.com/item?id=3556175
I care. I was a math student in my undergrad when I try to solve a particular problem on paths, in the end it uses a path version of cycle double cover conjecture (which was solved in the 90s).
https://chaoxu.prof/posts/2013-01-30-there-exist-a-path-of-l...
I also want to get it to work on cycles, but then I hit the cycle double cover conjecture so I gave up.
It’s the second most important problem in all of graph theory on this database of open math problems:
https://www.openproblemgarden.org/category/graph_theory?sort...
Obviously not an exact measurement but to give you some sense of the importance of the problem
Don’t bother. This is the third or fourth time AI has solved an open conjecture, and once again the comment sections everywhere are full of people explaining how this doesn’t really matter at all, how it’s an irrelevant, obscure problem, how any mediocre grad student could probably have solved it if only they had bothered to try, and how of course, human mathematicians will still be vastly superior to machines 100 years from now because they have that magic spark for which nobody can say what it supposedly consists of.
These discussions have nothing to do with mathematics, and everything to do with ego and fear. I’ve never been less impressed with humans than since AI started challenging them.
I think "importance" here is just being rated as 1 to 4 stars. So it's not "second-most important" but rather "one of the top 5 most important". That doesn't change much, but FWIW.
This doesn't contradict anything he said though. People on HN care only because an LLM proved a very difficult conjecture, not because we are independently interested in this conjecture.
Only? Seems remarkable to me.
Yes, the fact that an LLM managed to prove the conjecture is remarkable, but presumably you don't find the conjecture itself interesting.
[dead]
People don't talk about the cycle double cover conjecture here because this isn't a math website. Its lack of mention here is therefore poor evidence.
yeah, I think what makes this post different was that AI did it. hopefully science will advance faster in the next decades with AI researchers helping
[flagged]
You honestly think this wouldn’t be upvoted equally or more if a Chinese model did it?
Yeah
There have been multiple posts on here with 800+ upvotes in just the last few weeks for GLM 5.2.
The idea that all this enthusiasm is for certain Silicon Valley billionaires and not from genuine interest in AI technology is a baffling take.
To be clear, I am not agreeing that people only upvote their favorite billionaires, just that if this particular thing was done by a Chinese model it would not have gotten the same attention
> a Chinese model it would not have gotten the same attention
Well, you would be wrong.
Interesting point I guess, much to consider
Consider actually searching for GLM or other top Chinese models and see how many upvotes they have been getting.
Your claim that Chinese models don’t get as much attention is easily proven false.
Im using silicon valley collequially to represent "tech", not as a google maps pin.
So what billionaire are people rooting for when a new GLM comes out?
How many people do you honestly think even know who owns or leads Z.ai?
I certainly don’t.
[dead]
Hopefully. So far it seems to be doing more harm than good.
What harm? I think the major part of the US economy seems to be depending on AI.. without that, the economy seems bad..
We absolutely care about the implications of AI solving hard problems. I'm sure you can find thousands of posts on HN deriding AI progress the entire time, trivializing it as nothing more than a 'stochastic parrot'
i care about the CDCC but every time i post about it dang removes it and bans me
This was one of the most famous open graph theory problems lol. I am not a mathematician and even I ran into this when doing generative map design for game dev.
The only thing you've demonstrated here is some very funny confidently incorrect coping behavior.
Thanks for the fun facts? Indeed, this is not a math forum. Good morning.
> I can demonstrate this [that literally nobody cares about the CDCC here]
No, you cannot. Mindreading the readers of this site by sifting through people's comments is a barely passable proxy for this at best, especially when that audience has changed dramatically over even just those 14 years, and continues to do so.
[flagged]
the real world problems we care about are straightforward, the main challenge is wealth distribution and control over the power to do something about them
I agree. We have a coordination problem, and the way our AI lords are proposing to solve this, is by cutting humans out of the equation
> If people cared they would [have mentioned it before]. What are YOU on about?
I explained why and how I think this is both wrong (especially in the ridiculously absolute form it was posted in), and a weird point of contention.
This is a tech (startup) forum, with an increasing pull towards more general audiences. Math and sciences have strong ties to tech, but you won't see people discussing specific math conjectures here much, save for the ones that make the popsci or tech mainstream. It is only chance encounters like this where a person from the relevant neck of the woods might engage, provided they happen to be readers here, e.g. because of a passing interest in technology.
Given this, being surprised that you cannot find a mention of this conjecture in the post history of the site is difficult to describe as any kinder than just plain daft.
> If it’s so good at solving hard problems
A problem being hard (in the relevant sense here) doesn't mean they're lucrative to solve, or hold direct and broad societal relevance. Kind of a theme with maths and logic problems, and not by coincidence.
Conversely, a lot of practical hard problems are, well, practical. They're not logically hard, but in some empirical way. You're conflating different avenues of difficulty, and rejecting that there's even a multitude of them.
> Why is there no real world progress on things we do care about?
We?
Well, there's been very real progress on things I - and I'd think most this community - care about. I've been shipping tickets end-to-end with minimal involvement via LLMs agentically for a while now. It's been great, and an honest game changer. I've been delivering faster, more, and better. Exactly what you'd expect from a breakthrough technology: a wholesale improvement across normally competing dimensions. In a number of cases, the difference was outright stepfunction like. That is to say, if it wasn't for these models, they would simply not have happened.
This is its latest iteration and its newest - alleged - tour de force. That's why it's posted here to extensive reception. That it is nice to hear it being a boon in other sectors too. If this somehow escaped you two, I don't know what to tell you.
Thank you for taking the time to respond thoroughly. You made me reflect upon my frustrations and anger. I take back my flagrant comment.
> What are YOU on about?
Can you please edit out swipes like this from your HN comments? This is in the site guidelines: https://news.ycombinator.com/newsguidelines.html. Your post would be fine without that bit.
Personally I think it's a fallacy to assume that HN users mention everything they care about in HN posts, but that's not a moderation point.
Wait, what things do we care about?
Two years from now, when a proof of the Collatz conjecture is announced and verified:
"No one cares about that! What practical applications does it have? It's pretty trivial anyways. More hype from the AI psychosis crowd."
I don’t care if AI solves the collatz conjecture either, why should I?
If, after stealing all human knowledge, spending $1T+ on compute, hiring the best in the world while also stalling progress in other fields by pulling funding from fundamental research is a bunch of lousy math proofs then thats terrible trade. There is an opportunity cost here.
I don’t have anything against AI, and I do think it will progress a lot just like all other human endeavors. But this doomer permanent underclass humans are worthless myopic view of AI is not where its at
Materialisation?
Materialization of software?
Of matter.
What does that have to do with the feat itself?
No one here actually cares about folding laundry. I can demonstrate it by pointing out at the absence of posts on that subject.
...but when an affordable robot that folds laundry becomes available, people here pay attention.
Oh, for laundry to be solved!
Tell me about it! It is endless!
The point of this is if AI is solving things that nobody cares about, that's the utility here. It's doing something nobody else wants to bother with
Almost sounds like they pointed a prompt at every boondocks conjecture and wrote a press release for the one it plausibly solved.
"Assume for purposes of this task that a complete affirmative proof exists"
everybody knew the problem was impossible to solve
then one day somebody new arrived and they forgot to tell him/her, so he/she solved the problem
I've used this strategy for difficult bespoke problems and it does indeed work to incentivize the agent not to give up prematurely.
It's not gaslighting, it's motivation.
I also like how they ask the model to work on it for 8 hours; guess asking for more is against labor laws…
[flagged]
[dead]
> Statement of AI use. The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex (with GPT 5.6 Sol).
Quick! Someone (a human) copyright and patent it. /s
Good post, it perfectly captures the problem with AI. Here we have a claim that the double cover conjecture has a proof. Verified by… no one per the link.
Now imagine this proof is wrong. How would you know? Ok, think about the process in which you determine the correctness - why not do that initially?
And there it is. The problem laid bare. Ironically it reduces to the P and NP one.
You seem to be suggesting that it is just as hard to understand an existing proof to a problem, than to solve it yourself? I don't follow your argument at all, what are you trying to say?
Most likely they wrote the proof in Lean and had it verified by a computer
You believe this based off what?
Based on these people not being idiots or charlatans?
Why wouldn't they verify it, knowing that any shenanigans would certainly come to light?
Frontier labs have had multiple major announcements in the past about supposedly novel LLM generated theorems that turned out to be vastly overstating what actually happened. That's part of why they were so (appropriately) cautious with the unit distance proof.
This is spot on. And yet, when I try to publish my papers on P = NP with the proof reducing to "trust me bro, I checked this out carefully" I get shot down by irrate reviewers who demand to see my work. Why can't those people just believe what I say?
Maybe if I was an AI?
[dead]
This has been the standard in the world of "AI-produces-math-proofs" for a while
The prompt does not mention Lean.
I mean, if you've watched the past decade, this just seems like what news is today. "people are saying the double cover conjecture has a proof"
They post this and then say it's too dangerous to make open source. this is proof that in reality it's To protect their market position
Have OpenAI been on a crusade of "too dangerous to open source" recently? They've pivoted their more to messaging to "competitive reasons" recently, which I appreciate, because it's honest.
FWIW, Gemma4 31B is already quite a capable cyber/security model; do some post-training with RL gyms on it focused on cyber tasks and harnesses for a week or two, and on the specific domain of security/vuln-finding/pen-testing, you'll end up with an extremely capable frontier-cyber model that's entirely under your control at a shocking 31B.
Because securing your codebase, or securing your company's codebase is critical, and I consider it both an ethical and professional responsibility as a developer. It shouldn't depend on whether a classifier fires or not.
all easily varifyable tasks can now be solved with money. this is worth paying attention to. math proofs are verifyable -> math proofs are easy now. you can think of other such tasks: cybersecurity, AI R&D/RSI, killing people, 3d-printing helpful tools, maxxing-out human health, manipulation, self-driving cars, anything that can be checked
all jobs in the future will be those can not be easily verifiably done. if you need a team of people to decide if you have been productive, and those people cant be automated, you're in luck.
I don't really like these articles, because they seem extremely hard to verify. OpenAI has published a lot of stuff in the past where, upon close inspection, what they're saying is technically true but a lot less interesting or impressive than the headline. Except by the time anyone looks into it, the hype has moved on. It seems like there's maybe a thousand people in the world that can even say if this is good or not?
1. A lot more than 1000, you're off by more than one order of magnitude. It's definitely beyond my level of graph theory knowledge (undergrad level) but looking at the paper, it's not using any crazy machinery, and it's less than 3 pages.
2. Those people will say whether it's a good proof or not. We have other examples of interesting proofs from AI, we're really beyond the point of arguing whether it can produce any interesting math (though it seems to do much better at combinatorics than anything else).
Right, but my criticism is to the hit-and-run nature of these hype pieces. By the time there's any semblance of what it actually means everyone has moved on but then you have a bunch of people operating under delusions from the hype. I get why OpenAI does it but I wish people would stop upvoting it. Like, hacker news is not a mathematics forum so the only purpose of this kind of thing is hype boosting or polarizing people. I am not looking forward to the "MATH IS SOLVED!" people for the next few days.
You are basically right. The real acceptance of the proof comes when it's accepted to a journal after review.
However, in some sense spreading a proof needs to be done in math - then the community reviews and decides if it is valid.
We can't ignore the timing here though: this is a publicity piece for GPT 5.6!
I think you may be overindexing on the criticisms here. OpenAI has absolutely done impressive work in math already, and the criticisms are almost always based on the article that they initially published, usually available here in the HN comments within a few hours at most. Headlines will be headlines and hype guys will be hype guys, but OpenAI and Anthropic aren't lying and their bots are doing impressive work.
This one is a well-known problem with a brief, approachable proof, and they published the prompt.