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.
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.
>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!)
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.
> 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!"
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.
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 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’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.
> 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?!!"
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?
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.
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 either may eventually turn out to be enormously useful in ways we can’t immediately predict. Both are also 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 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..
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"
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.
> 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).
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.
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.
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 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.
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.
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".
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.
> 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.
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.
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.
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.
I am not very familiar with this problem but I am having trouble following the proof. Lemma 2.1 assumes the existence of a certain assignment of finite field elements to a cubic multigraph, but is this assignment always possible?
Actually I am having trouble making sense of the condition: we assign the edges pairs of F_8 elements. Then "for each" vertex v we are... counting the vertices v? I find this incoherent, maybe I'm too tired. And regardless it doesn't seem obvious that every cubic graph can satisfy such an assignment (whatever it may be). Even if I'm too dumb to understand the condition on Lemma 2.1, the proof seems incomplete until you show Lemma 2.1 holds for all cubic graphs.
But maybe I'm missing something obvious. I didn't read that 1985 survey paper and probably should.
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'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.
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
> 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.
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.
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.
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?
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 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.
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.
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.
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.
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.
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?
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.
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.
"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.
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.
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.
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.
>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!)
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.
> 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!"
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.
>(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 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’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.
> 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?!!"
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?
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.
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 either may eventually turn out to be enormously useful in ways we can’t immediately predict. Both are also 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 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..
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"
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...
No matter what humans do, it somehow ends up being a popularity contest.
It's almost like a twisted mirror of Conway's law.
> 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).
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.
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.
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.
> 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.
Proving a novel math theroem now is incredibly hard because all the easy ones have already been proven.
> 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.
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.
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".
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
> 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.
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.
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.
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.
I use GPT 5.6 as default and subtask agent and Fable as Advisor with Oh My Pi harness
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?
I am not very familiar with this problem but I am having trouble following the proof. Lemma 2.1 assumes the existence of a certain assignment of finite field elements to a cubic multigraph, but is this assignment always possible?
Actually I am having trouble making sense of the condition: we assign the edges pairs of F_8 elements. Then "for each" vertex v we are... counting the vertices v? I find this incoherent, maybe I'm too tired. And regardless it doesn't seem obvious that every cubic graph can satisfy such an assignment (whatever it may be). Even if I'm too dumb to understand the condition on Lemma 2.1, the proof seems incomplete until you show Lemma 2.1 holds for all cubic graphs.
But maybe I'm missing something obvious. I didn't read that 1985 survey paper and probably should.
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.
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.
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.
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.
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.
It is not necessarily the case that the instruction needs be taken literally
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.
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.
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
The voice models certainly can't: https://kittygr.am/reel/DWr31A1B1Ux/
they can now https://www.youtube.com/watch?v=8vvWTz6N7Qg
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.
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.
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.
> 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.
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?
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.
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)
> 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.
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.
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 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).
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
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.
…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.
What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.
But they used LateX
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 ...
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?
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.
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"
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…
"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.
OpenAI knocked it out of the park with this one.
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?
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
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 would assume/hope they had someone verify it before publishing
"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…
> 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