285 comments

[ 0.20 ms ] story [ 68.9 ms ] thread
> 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.

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.
they can call CLI tools to notice the passage of time. the harness can include timestamps too
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.
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.

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.
Same - at the end of the day I'd leave my last turn running with something like "I am going to bed so keep going until you are done" and be surprised that in the morning it'd kept going.
Once on a late-night session, I had Cline!Claude spontaneously point out the time to me and suggest that I get to bed and come back fresh the next day.

I don't think it's in the system prompt, but that the harnesses time-stamp each turn in the context.

And from what I've seen, they also include the current and max context, so that the model can decide whether to continue work, suggest compaction, or prefer actions that might reduce the growth of its context.

> Once on a late-night session, I had Cline!Claude spontaneously point out the time to me and suggest that I get to bed and come back fresh the next day.

I had Claude say something "It's getting late, let's pick this up tomorrow" at like 11am.

As for context, in my experience Claude starts trying either to do maximum work with minimum tokens when it's approaching limit, or it starts deferring useful work while doing busy work. Both result in a mess and complete loss of traction after compaction.

This is my experience with Claude as well, and the reason I switched to codex. Codex just seems far more efficient, despite the smaller context window, and it actually follows instructions.
It's in the training data! Long conversations between humans result in humans getting tired and going to bed.

I have this reality baked into my workflow:

1. Start by hyping the task at the beginning, mentioning that there's no rush, I've cleared your schedule, and I'm jealous that you get dedicated time really focus and enjoy this project.

2. Periodically say "Great work, let's finish this next week. Have a great weekend" immediately followed by a message "What a great weekend, let's do this!" sort of hype, for it to continue. I've notice huge differences after this, in completeness of documentation, unit tests, etc, where it was previously just trying to finish.

3. Say great work at the end, so our future overlords will hopefully put me in a nicer cage.

I was - pleasantly - surprised (and also a bit suspicious) a couple of days ago as I was having Claude resolve a problem in a running service that it had accidentally caused, and it eventually gave up since it involved hitting a 3rd-party API unconventionally. Then I told it that I needed the service working again as it was blocking another task, and immediately in that turn it resolved it.
It is not necessarily the case that the instruction needs be taken literally
> 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.

"Assume for purposes of this task that a complete affirmative proof exists"
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…
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?

pretty sure already millions of dollars (in inference costs) were already thrown at the Riehmann hypothesis

as the models get stronger, larger amounts will be thrown at it

imagine paying "just $1 bil" to go down in history as the company who's model solved the hardest/most famous open problem in mathematics. imagine the worldwide press headlines.

as they say, the Riehmann Hypothesis is the hardest way to earn a million dollar

I mean if there's something I'd bet against being solved by LLMs in my lifetime it's that one. We truly do not have line of sight into what a proof would even look like.
Why would you bet against it being solved by LLMs? Isn't this very post proof that LLMs in an agentic harness are capable of doing real math? If you just keep cranking away at the tokens I don't see a principled argument against that leading to more solutions to unsolved math, even the hardest problems.
There are different classes of mathematical problems.

The one in the post definitely shows the advantages that LLMs have compared to humans for some problems but it's in an entirely different class than the Riemann Hypothesis.

Riemann is one of the most studied math problems of all times and all of humanity has basically collectively failed to make progress. The idea that there's some technique that just hasn't been tried yet (like in the post) is very very unlikely.

The general consensus is that we'll need an entirely new branch of mathematics to solve Riemann - our current tools aren't just inadequate; they're of the wrong class entirely.

I suspect inventing new branches of math will remain beyond LLMs for the remainder of my life.

“ I suspect inventing new branches of math will remain beyond LLMs for the remainder of my life”

Well every branch of mathematics thus far has been invented by a human or a human using a computer, and humans will use this type of computer to solve math problems (or at least try), so I’d say this is a really poor probabilistic bet.

I find it kind of interesting the whole output wasn't released. A common criticism of mathematical writing is results are "pulled out of a hat"; you only write up a polished, final proof, but hide everything that went into developing it. It's kind of ironic the practice is even carried on when an LLM writes the proof.
But is the proof accepted to be correct? That is what distinguishes this from being notable to any other AI slop proof.
I would assume/hope they had someone verify it before publishing
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 ...

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.
Graphlib? Do you have a link to this for me?
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.

(comment deleted)
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?
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.

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.

A lot of mathematics often takes 100+ years to find a practical use because we have developed it so much that we have use all the easy maths. Things like CS or SWE are so new that you can still find stuff today that can be used tomorrow. Things like computation and cryptography was all discovered like 100 years before we had a practical use for it. Its an example of late stage scientific discipline. Things like physics, chemistry and biology will get here as well eventually.
It’s 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).

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.
> 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?!!"

> We attach basically zero value to writing a new program that hasn't existed before

We don't? People write new programs that go on to be successful software companies that make millions of dollars! Basic CRUD apps make money for their creators in their niche! There's so much money in software that it's taking over the world. The market is different, you're not getting worldwide household recognition for every little fart or sneeze of programming you output, but how can you say that we attach zero value to new programs when the history of computers is insanely valuable companies making new software and selling it. Windows, Oracle, mongoDB, etc.

> It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture..

I'm not sure about this, TBH I ask myself this quite frequently. In a world where machines are routinely solving very high end math problems every day, producing more proofs than humans would ever really be able to absorb or fully understand.... would that be a good thing? Would that in itself be valueable? It feels like that is a probable future, but I'm not sure that would actually be something we want. I think there's probably more than "value is that it's solved"

I mean, OpenAI delayed the public release of GPT-2 back in 2019 because it seemed capable of authoring interesting blog posts (that also happened to be untrue). It was a pretty big deal the first time Transformer models were capable of generating that kind of output--no one found it weird. We've just grown to take it for granted that large Transformer models are this capable.

The same cycle is happening now for a harder frontier. And proofs represent a pretty good benchmark for model capabilities, so a new model proving a result that a previous model didn't is generally notable in the same way that a model scoring higher on a benchmark is.

I'm sure we'll take it for granted in the not-too-distant future.

Proving a novel math theroem now is incredibly hard because all the easy ones have already been proven.
Isn't it immediately obvious that solving something that humans have been unable to do for decades or more is the most tangible proof of ASI, or at the very least pretty good AGI?
Is this something humans have been unable to do?

There’s only so many people with the necessary skills to solve this. And you need these humans to choose to spend their time solving this, and not something else.

>Is this something humans have been unable to do?

It's a famous open problem so yeah

>There’s only so many people with the necessary skills to solve this. And you need these humans to choose to spend their time solving this, and not something else.

Sure, but that doesn't mean a lot of very skilled people hadn't attempted and failed to solve this.

And you’ve known about this problem for how many minutes?
Long enough to know this has been on the Wikipedia page of open math problems for several years, but go on lol.
It's newsworthy because it's a milestone. It was something no human was able to do (despite trying very hard), but a machine did. Humans have written lots of interesting blog posts.

The idea that mathematics has rejected any notion of utility is absurd. It's not like topics get picked at random. Conjectures like this are interesting because they are a test of our understanding. The problem sounds easy, but apparently was quite hard.

So I suppose the value is that something like this gets used as a primitive to solve something that actually has impact. Ah, mathematics, never change!
> 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...

(comment deleted)
> and that can be arbitrarily far removed from practical utility

In which case it’s ~equivalent to not caring about utility

Mathematics is what everything else is built upon. I'm no mathematician but a very good friend of mine is: teacher at a big uni, researcher. Pure math.

His entire life he's had --and still has-- to deal with comments like the one you just made, implying that the only value is solving pointless conjecture (if it wasn't pointless, according to your logic, then the value wouldn't be that it is solved).

Truth is to be found in this xkcd:

https://xkcd.com/435/

"every novel result is broadly perceived as a big deal" is not at all true. AI companies hype any novel result as proof that AI is good for mathematics, but professional mathematicians write tens of thousands of papers every year, and for 99.99% of them, nobody cares or writes it up. Mathematicians certainly don't go around saying each and every novel proof in their papers are a big deal. Do you have any evidence supporting your statement that it is "broadly perceived" (by whom?) as a big deal?
> there's something funny about mathematics in that every novel result is broadly perceived as a big deal.

Is this true? Or is it just that mathematics is an isolated enough field that only the results that are a big deal get broadcast widely to the public.

I know little of the inner workings of the field of mathematics, but my naive assumption would be that there's probably lots of novel but boring results being discovered/proven all the time and we don't hear about them because no-one outside of the person doing the work and a handful of their colleagues is really that interested in it. Likely a lot aren't published in any way, because they're just stepping stones towards the goal of the actual area/paper/whatever being worked on.

Sorry but I completely disagree with your statement that "every novel result is broadly perceived as a big deal". Most results certainly are not consider this way (even though the average result has difficulties that are much higher than novel computer program you may have in mind -- no offense)
> 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

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.

I wonder if in each case they had parallel sessions, one trying to prove, one trying to find a counterexample
For comedy’s sake, I asked ChatGPT 5.5 about the significance of the problem and the chance that 5.6 would solve it with a three page solution. It said close to zero.

I invited it to search the internet and it remains extremely sceptical.

[delayed]
The prompt does matter. They specifically told it to assume a proof exists so it would not too easily dismiss the possibility.
I considered it, but I figured that whatever I did there would be inconclusive. Instead I tried to figure out the blast radius of this being proven, and I didn’t get very far with that either.
> However, it seems the proof is extremely concise so it seems that it is exploiting a clever trick that somehow all the experts missed.

Why is that a "however"? My reading is that it found a genuinely new solution that is both elegant and previously missed.

Seems like exactly the kind of result a human mathematician would aspire to.

clever tricks has value for sure. But the main way progress is done in mathematics is by building new theory, the proof of Fermat's Last Theorem is much more important because of the math it created to solve the problem, rather than actually solving the problem.
Right. I think I understand - this question was expected to produce a new theory and the clever solution avoided that.

Like I said below, I think this is a fantastic result. It discovered that this question really wasn't asking the right question. That's a determination that has eluded the humans examining the problem - and a real step forward - albeit not the hoped-for step.

No?

That depends on the branch of math. Combinatorics is trick-oriented. Maybe this is why AI has done well in that.
Grant Sanderson recently distinguished mathematicians that create syntax (he might use the word ontologies in some circles) from those who manipulate it on the Dwarkesh podcast. I liked this delineation a lot. We seem to be at ‘manipulating syntax’.

Creating useful ontologies still seems a ways off here. Not to complain about this awesome result, just to think about where some future goalposts might be laid (and of course complained about / discussed at length when reached)

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.
…and thank God it's not Lean.
What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.
Perfect -- that's great to see. The proof strategy in Lean appears essentially identical to the natural language strategy (as much as is reasonably possible). I think this settles it!
I like how the proof is so concise. I made progress on some unsolved combinatorics problems but the proof was 45 pages long to extend the frontier by one step.
I did some math research in high school where the proof boiled down to dozens of cases of ugly polynomial inequalities. I can't find the PDF now, but the final paper was something like 70 pages, and several of those were full-page polynomial expressions expanded out. The actual prose was probably 5 pages or so.

It was categorically the least elegant proof of anything I've ever seen.

I'm incredibly grateful to for the opportunity to have done the research and gotten my feet wet early on, but boy do I cringe when I look back at that paper.

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.
That's a much shorter and more elegant proof than I was expecting, especially after reading some of the earlier Erdos proofs. GPT 5.6 Sol is the real deal.
Is 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?

On the last Dwarkesh podcast with 3blue1brown, one of them mentioned that frontier models are now able to work through a whole proof in natural language, just like a human mathematician would. But when they first solved IMO problems in 2024, they relied more on Lean to catch hallucinations.
As someone who was a research assistant in this field one summer back in college, I spent the day trying to check the proof, or at least the obvious places a mistake would be. It's surprisingly readable, so I guess we'll find out soon.

Lemma 2.2 specifically "feels" new to me. You can get part of the way by duct-taping several papers together (playing along at home: I found Tutte 1954, Bermond–Jackson–Jaeger 1983, Máčajová–Škoviera 2005, Zaslavsky 1982. interestingly, only Tutte appears in the works cited). But it's surprising you'd think to pick those, and surprising it works, because you still need a genuinely novel parity argument at the end. Those steps individually are all pretty simple, knowing to chain that chain together, isn't.

The guess-against the checker paradigm is real (ie AlphaProof), and something like that was probably involved here. But this area of graph theory isn't in mathlib, you need to write the proof checker first, and then you need to know what kind of proof checker you need to write (or just do a brute force search for new proof checkers). Probably how you got this result is have a recursive tree of agents until you divide into small enough subproblems.

At a certain point you need a philosopher to figure out what that "means", ie if you have a big enough tree of small enough subproblems, some of the "magic" so to speak moves out of the proof checkers and into the way the tree got structured.

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).
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?

It's hard for me not to think what's the point. I am a very average, even below average person in times of intelligence. What is even my value or reason to be if I know anything I can do, LLMs can do better? What is even my value both on job market and as a human?
Sorry to be nihilist, but you never had any objective value if you're thinking in these terms.

As far as we know, the universe "just is". There is no universal objective value of human beings, at all, any one of us.

You have to make or find your own value in the universe. I try not to think too hard about the nihilist side and try to appreciate that for some unfathomable reason, I seem to have what I call consciousness - the ability to observe the present and have it superimposed on the past, and what may be the future, leading me to "experience" things. I don't understand it, no-one does (some people suffering from the Dunning-Kruger effect think they do, but they don't), and yet, here we are.

So it doesn't matter to me if machines perform better than I do, because already lots of other people do. Just try to find your own joy or meaning, somehow.

> As far as we know, the universe "just is".

I don't know this. In fact, billions of people around the world don't know this. In fact, all evidence points to the contrary.

You have objective value being made in the image of a personal God. Denying that leads to a lot of pain, namely nihilistic suffering because it's on you to "pull yourself up by the bootstraps" in any endeavor involving your own self-worth.

To cite the famed Russian philosopher Norm Macdonald; "Scripture. Faith. Grace. Christ, Glory of God. Smart man says nothing is a miracle. I say everything is."
This is one reason why I can't stand hn. Edgelord nihilistic comments that say nothing matters and take everything for granted get up-voted while credible and rational statements about God get down-voted.
What? What is rational about faith-based comments?

Literally nothing is rational about that. It's also just flat out off-topic.

That is an incredibly insulting comment. I am married, two children, have lead a fantastic fulfilling life. Just because I don't believe the Flying Spaghetti Monster created the universe doesn't mean I am an "Edgelord".

Remember the phrase, you also don't believe in God. There are hundreds of gods you don't believe in.

Bringing up the Flying Spaghetti Monster does make you an edgelord though.
Because it reminds you that your specific deity is just as ridiculous?
Which deities don't you believe in? I don't believe in all of them. Presumably you don't believe in almost all of them?
"In fact, all evidence points to the contrary."

Um. No? I'd like to see how you conjured up that one. Because evidence does indeed point exactly to things just being as they are.

"You have objective value being made in the image of a personal God."

Conjecture. Unsubstantiated.

"Denying that leads to a lot of pain, namely nihilistic suffering because it's on you to "pull yourself up by the bootstraps" in any endeavor involving your own self-worth."

No? Sounds like you're projecting your own belief here. "If I didn't believe in God, then what purpose is there to anything?" It's very small of a belief.

Even Neanderthals? Were they also made in his image? We interbred with them. We can go all the way down the evolutionary tree here just say when to stop.
> made in the image of a personal God

How does that work? The physical image? Or the mental image? Either has big problems. An omniscient god is so cognitively beyond a mere "7+-2" human that the latter claim makes no sense at all.

There are smarter and better humans at just about everything you or I could want to do, that's just life. Most of life isn't about comparative advantages, it's about enjoying life with people we like.
I can't enjoy life with my people if I can't eat, drink, and have a roof over my head.
Do you have friends or people in your life that are also not geniuses? Do you think about them this way? Why or why not?
Manual labor
Even that is being automated now, it was one of the thing being automated very early on in factories..
And yet we still have human laborers. Robots are a lot more expensive than AI inference.
Anti-ai sentiment won't be automated out haha
Military will always like warm bodies ;)

Sometimes it's easy for me to imagine a bad future like this; where most of the men are forced into military as the only org that still has use for wetware, and women are valued only for their ability to birth new people...

You have inherent value by virtue of being human. Unfortunately it seems like people have forgotten humanism.
Your value is intrinsic as a human being. We’re capable of love and shared experiences that a machine will never know.
This is a great question. Thanks for asking it. It really got people talking.

My $0.02: Your value as a person never had anything to do with your value to the economy. It's time to relearn that fact.

Check out some of Tom Hodgkins books for more. Or maybe anxietyculture.com.

Yeah but what is a persons value economically anymore? What skillsets will enable us to continue to make a decent living till we are old?
It's funny because if people get replaced and don't have money they won't pay for API tokens either so the retail AI business collapses too, there won't be enough demand because people rather buy food.
Sorry, but most of us need to work to eat. This idea that our "value" is has nothing to do with the economy is an idea rooted in deep privilege, in the ability to say -- if I don't like my job, if I'm not employable, I can just retire, and the only problem will be figuring out how to live life afterwards.
But it is. My worth is based on what my value is, what I can do. What when I can no longer have any value on the job market?
Your economic value and your value as human being are two different things.

Yeah, you gotta eat, but some of us have been slaves for so long that we've started to believe that our self worth is defined by what we will fetch at auction. It is not.

Read more about the Protestant work ethic, it's history, and what life was like before men began to assume it was the one true view of life. Not very long ago nobody had clocks, and the idea that work was an ethic was a fringe, almost cult-like belief system. Now most humans routinely take stimulants every morning to be better servants, and mistake their job for their purpose on earth. That's just nonsense our culture invented though.

If the master wants you to do something, force him get out the whip. Don't let him live in your head rent free by adopting his crazy belief system.

YOU decide what your value is. Don't abdicate the decision to someone else.

AI will never be better than me at appreciating a good sunset.
Claude performs 50 microappreciations per second
Perhaps it will. And perhaps countless animals are already better than us at appreciating a good sunset, yet we do not seem to value them much.
Animals sure but they evolve with us for hundreds of millions of years so they get a break. They did their part.
You are a human being, one of the most wonderful thing the nature has ever created, besides all the other living beings and the wonderful earth we live in. Do not tell yourself you have a value just because some company may want to hire you or not.

Companies and industries already use tools and machinery for tasks were once done by human beings. AI is just another tool they will use and it will probably replace human beings from some intelligence related tasks.

However that may bring more disruption to the society if the government in your country do not protect and help people and leave free rein to capitalistic greed.

I'm my opinion that already happened in the US, not by using AI, but merely by using H1B visa to get intelligence worker from abroad. What happened is that the companies are doing great and getting the best smart people in the world but American people and society have been disrupted.

Live your life fully, be good to yourself and to others. Don't worry about the market.

Well, you provide training data to the savior and our Lord AI. /s
Remember that the most valuable human in the world is Elon Musk. What it means to be valuable is to be like Elon Musk. Calibrate your goals accordingly.
You don't compete with a chainsaw at cutting trees. You decide what the tree is for. Then sell the rainforest for shareholder value.
And now AIs can do all that
>> What’s left?

For example, there's all the problems that the same off-the-shelf model hasn't solved despite OpenAI running it for many hours on them. Don't forget you're only seeing the results of successful runs.

We can estimate that those unsolved problems must number in the dozens, or even hundreds, given the amount of time that passed since the last announcement of a solution to an interesting problem by an OpenAI model: i.e. the unit distance problem which was announced solved in 20 May this year. That's a couple of months, yes? We can be fairly certain that OpenAI have been trying to solve other problems all this time, first because they are hell bent on demonstrating that their models can do maths and second because we just got another result, but it took that long. They were obviously not twiddling their thumbs all this time.

So if OpenAI are running their model on a single proble for eight hours at a time (according to the prompt they released) they could be easily have run a few hundred instances of their model on the same number of open problems 156 times for each instance (53 days since 20 May, with a model running in three eight-hour sessions per 24 hour day). I mean the only restriction is the cost they're willing to pay for the inference.

So yeah, there's a lot left to do still, don't worry.

The 2 most notable/interesting solutions have come from Open AI directly, but a lot didn't and came from 3rd parties doing their own thing with publicly available models. I don't see why one would assume they're running models on hundreds of problems. Most likely they have a few problems they especially care about that they run on.
What, Erdős problems? It's hard to see how anyone except mathematicians, and then again only a few communities of mathematicians, especially care about those.

Remember back in the day when Deep Mind made AlphaGo? That made huge waves for two reasons: one, it was very well understood by AI researchers that beating expert humans at Go was very hard; and, two, that Go is a game of great cultural significance to literally billions of people outside of academia, albeit mainly in SE Asia.

Now, Erdős? I'm a computer scientist and I had to look up the planar unit distance problem when I heard about it because I had no idea what that was. Because it never comes up in the literature I read. I'm not saying it's not interesting, but it does seem a bit... random? That they started with Erdős problems? I'd have gone for a Millennium Prize problem, first. P vs NP, Riemann, Navier Stokes, those are heavy-weight results that would establish AI as the de facto approach to mathematics for the foreseeable future. Even I would find it hard to raise an objection (imagine that). Erdős can take a number, compared to all that.

I'm not saying they're choosing problems at random, mind. But it does seem like we're only seeing the tip of the iceberg, with respect to what the AI companies are doing internally. That shouldn't be a surprise. That's exactly how research works in general, both in academia and in industry. There is a clear survivorship bias and we only ever get to see the positive results, never the negative ones.

>> The 2 most notable/interesting solutions have come from Open AI directly, but most of the 'LLM solves open problem' category didn't and has come from 3rd parties doing their own thing with publicly available models. I don't see why one would assume they're running models on hundreds of problems.

Actually, that's a good point but it's in support of my contention. If there are random people in the community running LLMs on their own, favourite, maths problems, we should be seeing many more of those solved and much more often, provided LLMs were really as good at maths as OpenAI et al want them to be. There must be literally thousands of mathematicians trying to use LLMs to solve this or that problem that is famous in their community. Where are all those spectacular results?

Or, to abuse Fermi's question, where is everybody?

>What, Erdős problems? It's hard to see how anyone except mathematicians, and then again only a few communities of mathematicians, especially care about those.

Erdős problems vary enormously in difficulty and significance. The fact that a problem is obscure to non-mathematicians does not make its solution unimportant. There are also many major open problems in computer science that most laypeople have never heard of.

>That they started with Erdős problems? I'd have gone for a Millennium Prize problem, first. P vs NP, Riemann, Navier Stokes, those are heavy-weight results that would establish AI as the de facto approach to mathematics for the foreseeable future.

Solving the biggest, most famous open problems would "establish AI as the de facto approach to mathematics for the foreseeable future"? It would do a lot more than that.

>That's exactly how research works in general, both in academia and in industry.

Then what exactly is the objection? Research normally produces many failures and incremental results before a major success. Do you apply this survivorship-bias criticism to every published mathematical result, or only when a machine contributed to it?

>Actually, that's a good point but it's in support of my contention.

If they're running as many problems as constantly as you imagine then they did not miss all that. So either they're just not sharing it us which contends with your "desperate to demonstrate mathematical competence" or they have their eyes on a more curated set.

>Or, to abuse Fermi's question, where is everybody?

If we had as many verified alien encounters as LLM contributions to open problems, nobody would be invoking the Fermi Paradox. Where is everyone? Right here.

>> Then what exactly is the objection? Research normally produces many failures and incremental results before a major success. Do you apply this survivorship-bias criticism to every published mathematical result, or only when a machine contributed to it?

Yes I do. Not mathematical results specifically but generally research results. I might even have articulated that criticism on HN. I don't know if I could search for it easily though.

>> If they're running as many problems as constantly as you imagine then they did not miss all that. So either they're just not sharing it us which contends with your "desperate to demonstrate mathematical competence" or they have their eyes on a more curated set.

The people desperate to demonstrate mathematical competence are the AI companies. The people discussed in the part of my comment you quote are "random people" by which I meant the "3d parties" in your original comment.

>Yes I do. Not mathematical results specifically but generally research results. I might even have articulated that criticism on HN. I don't know if I could search for it easily though.

Okay Fair, but then this is a general research issue and not really a Open AI issue.

>The people desperate to demonstrate mathematical competence are the AI companies. The people discussed in the part of my comment you quote are "random people" by which I meant the "3d parties" in your original comment.

I'm not sure you got the point i was making. The point there was that if Open AI were running as many problems as frequently as you imagine they are then those 3rd party results should have been achieved by them, and if they're really so desperate to tell us how good the model is for math then why didn't they tell us ? Why have they only announced 2 results when they could have announced near a dozen by now ? Sure these 2 are in a class of their own, but some of the others are genuinely impressive in their own right and would certainly help that narrative you're talking about. Even Google has done something like that - https://arxiv.org/html/2605.22763v1

Either they're just not telling us and aren't as desperate as you imagine, or they're simply only interested/running models in a relatively few set of problems.

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.
I am not very familiar with this problem but I am having trouble following the proof. Lemma 2.1 assumes the existence of an 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).

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 didn't see the next paragraph after the proof. This typography is hard to read on a phone. Wish HN would let me delete the comment.
I was not a fan of the writing style of the proof. There seem to be some irrelevant details: Is the mention of 8-flow at all relevant? I, at least, found the definition of L on the first line of the proof of Lemma 2.2 to be needlessly inscrutable, and my thesis advisor would have likely stopped reading there and told me to fix it.

Maybe someone should ask the model to make a more clearly written and thus easy to verify proof :)

I was confused at first when you asked if the 8-flow is relevant, when like, the 8-flow is a key input that the cycle double cover is built out of. Then I realized, oh, I guess technically they're not using the 8-flow, they're using the Z_2^3-flow. But like. The existence of an 8-flow and the existence of a Z_2^3-flow are equivalent, and I gather most graph theorists are going to talk about it in terms of the existence of an 8-flow, so noting that having a Z_2^3-flow is equivalent to having an 8-flow helps the reader to put this information in context.

I'm not sure why you find this proof so hard to read. I found it mostly quite readable (and the definition of L is straightforward? I wouldn't have written it quite that way but it's hardly inscrutable), although I feel like some parts are maybe lacking some exposition to explain the reason for certain things -- it doesn't feel written "in order". I also don't like that it's not cleanly separated into theorems and proofs -- some of the proof occurs in parts that aren't set off, for instance, and there isn't even a proper main theorem statement! But overall I was able to get through it without a lot of trouble and I'm not even a graph theorist...

My issues with the definition of L are mostly about the order in which things are written.

L(t, epsilon)_e breaks down the range of L onto its component values indexed by edge, but this only really makes sense when you know that t and epsilon are. They are sort of defined in the middle of a sentence in the proof of 2.1, which IMO is asking a lot of the reader, and this sort of sloppiness is a way that errors can hide in a proof. (Not that I see an error here. But a formalization in Lean or whatever would not get away with this.)

And, in the same definition of L, for some reason the e=uv part comes at the end only after u and v are used.

What would be wrong with stating, in the definition, what sorts of objects t and epsilon are and with omitting e entirely in favor of just calling the edge uv everywhere?

are the references real? how do you think it got access to those papers? were they somehow already in the training data, or a result of web searches, Google scholar, etc?

None of them include a web URL but in text some are super specific ("[3, Sections 2.1 and 3.1]" and "[8, p. 367]").

The references go back to 1954 (Chronologically sorted: 1954, 1973, 1975, 1976, 1978, 1979, 1981, 1985, 1987 and 1994.)

Since reference 10 is included as "personal correspondence" maybe the reference itself was copied from one of Tutte's other papers? Or how did it get that reference?

If it were a human (going off of memory as it has been a while), they would probably be using mathscinet and their university library to obtain copies of these papers online. Many old papers are digitized and available by these means. I’m sure the AI companies have it all easily accessible and/or the entirety of mathscinet is in the training data. The “personal correspondence” is possibly lifting from another paper or journal but yeah that is a bit odd that they wouldn’t source where they lifted that from directly.

I can’t say if the citations are accurate because I didn’t check.

Yes, reference 10 jumped out at me as well. I thought personal correspondence references typically include one of the authors of the paper.
It's definitely cribbing from other papers.

https://scholar.google.com/scholar?q=W.T.%20Tutte%2C%20Perso....

Sloppy scholarship. On the other hand, it's simply a credit attribution of posing the problem, so it's not material in evaluating the results. I observe that the majority of references I can find that attribute this to Tutte are very indirect - i.e., citing sources that themselves claim Tutte was one of the people who formulated it - so it would take someone with a little more time on their hands (or perhaps an LLM) to track down the original...

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.

What you're describing is similar to how the copilot harness in vs code tracks state and previous work. These systems are being implemented, bit by bit.
> I always wonder how they make these long-running prompts and I guess they literally just tell it to "keep going".

Many harnesses support a /goal as well. When the agent thinks it's done, another LLM compares its results to the goal, and if not, tells it to keep going. It's quite easy to have agents working on something for hours this way.

I'd love to see the failed runs too. The success is impressive, but the distribution of attempts would be just as interesting.
I don't really like these articles, because they seem extremely hard to verify. OpenAI has published a lot of stuff in the past where, upon close inspection, what they're saying is technically true but a lot less interesting or impressive than the headline. Except by the time anyone looks into it, the hype has moved on. It seems like there's maybe a thousand people in the world that can even say if this is good or not?
You are basically right. The real acceptance of the proof comes when it's accepted to a journal after review.

However, in some sense spreading a proof needs to be done in math - then the community reviews and decides if it is valid.

We can't ignore the timing here though: this is a publicity piece for GPT 5.6!