- 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
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?
> - 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'm just saying, let's not get painted into that corner completely as a species :)
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.
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 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 invited it to search the internet and it remains extremely sceptical.
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 :)
> 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.
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.
Some do. But there's also the notion that a clever trick is a bad explanation.
And discovering a bad question leads to the correct question. No?
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)
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?
Exactly, "clever". Isn't that the whole point?
Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...
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.
This "spend at least 8 hours" trick is a new one to me, though.
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 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.
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?
Throughput Output tokens Output cost
---------------------------- ------------- -----------
40 tok/s (5.5 low) ~9.2M ~$275
55 tok/s (5.5 base) ~12.7M ~$380
70 tok/s (5.5 high) ~16.1M ~$485
750 tok/s (Sol Fast, $75/M) ~172.8M ~$13,000
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.
I assume they didn't use the Cerebras version for this since it's probably very supply-constrained right now
https://x.com/thsottiaux/status/2075596669958472146?s=46&t=Z...
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.
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
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.
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?
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.
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.
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.
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)
Obviously it can impersonate art, but where creativity and the human story matter artists need not worry.
Personally this gives me additional confidence that this is the real deal.
https://concludia.org/graph/g_2ecb8083-52ec-3448-8c30-2f9bc7...
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.
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.
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.
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.
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.
With the Erdős proof, OpenAI added perspectives from working mathematicians that gave some context -- hope something like that appears for this one eventually.
(Erdős problem 90)
Clearly that sentence isn't AI generated ...
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.
There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.
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.
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...
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.
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.
In which case it’s ~equivalent to not caring about 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!)
Do you have some examples that the adult could instigate, rather than waiting for the child to express curiosity?
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 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!"
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.
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.
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.
Yes, the math department.
In any case linear algebra, stochastics, calculus; plenty of engineering and science applications for all these.
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.
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.
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.
If it was the professor, then that would be very embarassing on his or her part.
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?!!"
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.
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.
That's unnecessarily reductive. you could have said "most of the value is that erdos' name is attached to it"
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.
"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...
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.
It's almost like a twisted mirror of Conway's law.
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.
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.
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).
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"
I suspect the value is in showing the potential that LLMs have in developing new breakthroughs.
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.
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".
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.
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?
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.
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.
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 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.
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.
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:
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?
I can’t say if the citations are accurate because I didn’t check.
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?
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.
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.
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).
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.
Pro = test-time compute (best of N responses)
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.
then one day somebody new arrived and they forgot to tell him/her, so he/she solved the problem
It's not gaslighting, it's motivation.
Quick! Someone (a human) copyright and patent it. /s
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.
Why wouldn't they verify it, knowing that any shenanigans would certainly come to light?
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.
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).
This one is a well-known problem with a brief, approachable proof, and they published the prompt.