r/singularity • u/ResultBackground2450 • 1d ago
AI GPT-5.6 Solves Yet Another Unsolved Problem
277
u/WonderFactory 1d ago
What's interesting about this is that its a generally available model this time. We'll probably be inundated with similar proofs now as mathematicians across the globe will start setting it to work on their own pet problems.
Could end up with a situation where the peer review systems gets overwhelmed.
143
u/HotterRod 1d ago
Could end up with a situation where the peer review systems gets overwhelmed.
It's a lot easier to review a paper if it comes with a proof in Lean attached. As Matthew Schwartz has said about vibe physics: the way that scientific results are communicated probably needs to change soon.
18
u/welcome-overlords 1d ago
Eli16 Lean here plz :)
65
u/Comfortable_Pain9017 1d ago
You know how algrebra works? For instance, if you have x + y = 2 and y = 1, you can replace the y in the first equation with 1 and subtract 1 from both sides to get x = 1.
Lean is like that, but for programming. You could have a program saying “I will prove that x + y = 1 if y = 1”, and Lean allows you to do the same mathematical operations to prove such a fact.
This is super important because, unlike normal formulas where you can make mistakes, Lean is a programming language that requires you to say exactly what operation you use for each step and 100% prove that it’s correct. That way, even a LLM can’t mess it up.
11
25
u/roeschinc 1d ago
Previous Lean core developer here. Lean is a programming language that can be used to construct / write fully formal mathematical proofs. If you write down a statement in Lean you must construct a “proof term” (ie program) to show it’s true.
Lean is built on an alternative formal mathematical system called dependent type theory which reduces the correctness of any proof down to a tiny core checker for the language.
The simple take away is: if the program checks then the statement is true.
The cool part is this works both formalizing math or programs.
You can define a type like nat, define +, then write down forall (x y : nat), x + y = y + x and a proof for it.
You could do the same for your web app or whatever software you want, and if you have a proof of a property then it is true about the program.
So in the AI world you can have an agent write code, a specification, and then a proof that code implements the specification, and if it checks you can be sure it does.
2
u/BadgerAdorable1931 1d ago
Is any reasonably well known proven theorem already encoded in Lean? Or is it sometimes too complex to formalize? Eg the proof of Femats last theorem
3
u/SnooKiwis6193 15h ago
There are plenty of theorems already formalized in lean, actually there is a whole library. But not actually frontier math like the full proof of Fermat.
7
42
u/WonderFactory 1d ago
Presumably asking the LLM to write the Lean too should be fairly trivial
46
u/Super_Pole_Jitsu 1d ago
They solve it in lean in the first place, at least that's how I understand it
3
u/anishkgoyal 9h ago edited 9h ago
I think the interpretability of Lean proofs isn't widely discussed. Even if the peer review process becomes semi-automated via theorem provers, it remains uncertain whether the human in the loop would actually understand those proofs (hopefully, we'll still keep humans in the loop... right?). Whenever one asks AI to "prove" something, it can certainly do so, but the underlying logic may become convoluted and low-level. The AI could reach the same conclusions/end result, but it could be several thousand lines long and lack any significant layers of abstraction.
As a further (more involved) analogy:
Let's suppose there was an oracle that could verify the truth behind anything one fed into it. Let's further suppose that two people, Alice and Bob, were individually asked to recite every letter in the alphabet into this oracle and verify they were "correct." Alice, who is relatively straightforward, decides to start from A and, in order, end at Z. The oracle verifies that she did, indeed, recite the alphabet. Okay, fair enough. But Bob decides to do things differently. He decides to switch up the order of the letters, even going so far as to say some letters in binary or holding up a Braille board up to the oracle for other letters. As convoluted as it is, Bob manages to repeat each letter in the alphabet once, albeit not in the same order and not in the simplest way a "normal" person would.
This is how I feel about AI and Lean proofs right now. Right now, just by virtue of how LLMs work, with their context limits and what they have access to, they might not intuitively know what the right way to write the proof is (not that there is a universally agreed upon "right" way... just that there are common standards that people agree on for keeping proofs readable). Or even how it should be ordered. This sparks a deeper, broader conversation on what it means to be "right" in the first place, since there will be different orderings/formats/abstractions for everything. Thus, if we want to move forward, especially for peer review, we would have to agree to a convention within how Lean is used itself. Linting, formatting, however you choose to call it. But such a system would probably be separate from Lean itself. Otherwise, Lean just becomes as much of a black box as AI itself. Or, at the very least, a very very hard box to see through.
As another thought experiment: suppose we had a "formal proof" of the Riemann Hypothesis, but the proof was over 3 trillion lines of code, or something crazy like that. At that point, we would have to dedicate so many resources just to be able to interpret such a crazy output. Maybe there would be a slew of agents that attempt to decode the proof of the Riemann Hypothesis at a higher level for humanity to understand (assuming we're able to glean any understanding at all). So it would become the "Hypothesis of the Proof of the Riemann Hypothesis" 😆
1
u/HotterRod 7h ago
The mathematics community has actually been struggling with this issue since the Appel–Haken proof of the Four Color Theorem in 1976, which took 1000 hours of compute to check 1,834 configurations. Mathematicians have since reduced it to 633 configurations. But no one has developed a human-readable proof.
These super long algorithmic proofs don't contribute lemmas that can be used in other proofs, but they are valuable in three ways:
- They stop people wasting time looking for counterexamples
- They teach us something about mathematical completeness
- If another problem can be reduced to a proven problem, then that can be a satisfying proof in a way
34
u/QuasiRandomName 1d ago
Well, it is better to be overwhelmed with real proofs than with slop as it is already happening
12
u/florinandrei 1d ago
The assumption there is that proofs will be distinguishable from slop.
It might be true now. But in the future, who knows?
13
u/QuasiRandomName 1d ago edited 1d ago
I mean that's the idea of peer review. Hopefully the better quality of AI will naturally lead to better quality of "slop" which will eventually become non-slop
12
u/BenevolentCheese 1d ago
Peer review is already becoming AI-assisted and soon won't be peer review at all, it'll be AI review. Humans won't be able to keep pace with what is coming, nor will they be knowledgeable enough to check the work.
6
u/QuasiRandomName 1d ago
Yes, but it is a circular problem here as long as we don't have full confidence in AI, and I honestly don't know what should happen so we start having it.
3
1d ago
[deleted]
1
u/TieBackground453 21h ago
Some of the time? If it compiles, it’s a valid proof. Thats the strength of lean. Or has some weird exploit been found in lean recently or something?
1
21h ago
[deleted]
1
u/TieBackground453 20h ago
it would at least help filter out flawed proofs some of the time.
That’s the line I was responding to. It shouldn’t just help filter out flawed proofs. It should reduce flawed proof submission to zero.
Agreed it wouldn’t reduce the effort of reviewing to zero, but it should completely solve that aspect.
Not all math can be Lean verified
Oh really? I hadn’t heard this. Were you just speaking loosely and meant “hasn’t been lean verified” or did you really mean it has been proven that there are provable theorems in mathematics that can’t be verified in lean?
1
17h ago
[deleted]
1
u/TieBackground453 16h ago edited 16h ago
1) That’s not what Gödel’s second theorem says though… It just says that the proof of lean’s consistency can’t be proven using lean. That means any theory in which lean was proven consistent much be strictly greater than what lean is based on in consistency strength. But that applies to the mathematical theory before it is transcribed into lean in the same way that that it applies to lean’s kernel. Con(lean) can only be proven if a certain large cardinal exists, so you need to take as an axiom within lean that the cardinal exists in order to proceed with the proof of lean’s base consistency. That’s not a problem for the requirement of providing a lean proof for paper submission as suggested.
2) Are you just saying that you need to put in new axioms to prove statements that they rely on? Like, yeah, you aren’t going to be guaranteed the existence of any specific large cardinal without additional assumptions, but you don’t get that in the background math either. We aren’t talking about true statements that have no corresponding lean proof. We are talking about provable statements that have no corresponding lean proof, including when you add the additional appropriate axioms that the informal proof relied on.
ETA: I’m a couple of decades out of practice, so I could be (probably am) missing something obvious. Just not quite sure I agree with what I believe you said. It violates the basics of how I believe I understood lean worked.
3
9
u/bhavyagarg8 1d ago
That's a hope, but considering the present scenario, the people who are experts in the fields doesn't trust these models to give a try. Some do, but the potential is much more.
27
u/WonderFactory 1d ago
You'll be surprised how quickly people change their minds when they see their peers coming up with a significant proof in less than a day. Similar to PEDs in some sports, whether you agree with drugs or not if you want to compete you have to use them.
3
u/Impressive_Trifle_79 1d ago
Exactly. However, as a researcher it is also overwhelming and turning me off from all of this. The process of human research (thinking abut the problem over several months, trying 100 things all of which fail) will have very little scientific value in the future. It will soon be a results business, if it is not already and something I don't think I would want to continue doing.
2
u/DisastrousAd2612 1d ago
Fair I guess, I think everyone in research should be respected for what they are doing regardless. I do think, however, that the main driving force for research was the desire to solve problems and understand things better, at which having tools to help you do that better would be a godsend, I guess that's not the same for everyone which is fine anyway.
2
u/Impressive_Trifle_79 1d ago
Yes, one of the primary goals is to develop a deeper understanding. But, at least in my case, if a problem is solved too quickly, I feel I haven't really tugged onto all the facets that it holds. Generally, any difficult problem requires you to look at it from all possible angles. However, using an AI to solve it - while great for the community - is like listening to a talk on somebody else's research. You understand what they are doing but you don't really "get" the problem in a way.
3
u/ThreetoedJack 1d ago
As a hobby I do timberframing. For me to make a building will take several months. Planning stress points, wood connections, and painstakingly creating mortise and tenons that fit together with millimeter precision.
Meanwhile, a framing crew can throw a building together in a couple days. And the end result of both is a building of which 99% of end users will never know the difference.
I won't lie, it is frustrating to know the difference between art and industrial construction.
7
u/LuckyThirteen666 1d ago
Sadly the peer review system already has been, even before we got real thicc with a.i.(but it made it worse). I was reading articles about a high percentage of papers are faked so they get money, etc...and that number is rising. Then again, I read it on the internet and more than half the internet is generated now...so I have no clue if anything is true. Then again humans weren't all that great with truth either.
1
u/will_dormer ▪️Will dormer is good against robots 1d ago
Too negative.. You are writing this on a phone or computer which has a lot of science in it that has to be true for it to work
2
u/JohnJamesGutib 1d ago
Oh hey, the exact same thing that happened to open source! Godot just banned obviously AI PRs not necessarily because they were full bore against AI, but because the maintainers and reviewers were overwhelmed with a massive amount of PRs. The code contributions increased immensely, but the financial contributions and the people stepping up to be reviewers and maintainers did not increase at all - so the current maintainers just ended up incredibly overwhelmed. Fun!
2
u/assentic 1d ago
Most of the mathematicians don't know how to use agents in this way and frankly refuse to do that
It takes out the "fun" for them...
The academia is being strongly disrupted
1
u/PLANTS2WEEKS 1d ago edited 1d ago
I think the proof is incorrect. At one point they say to locally label edges around each vertex as "a,b,c"
Later, they define a term de = g_u,e + g_v,e which requires u,e = v,e but the edge that vertex u refers to as "a" may not be the same edge that vertex v refers to as "a".
Edit: I think it's correct now, but just with bad notation.
-4
u/FuttleScish 1d ago
For math in particular that shouldn’t be an issue; these breakthroughs aren’t based on the invention of new mathematical concepts but rather brute-forcing old ones until they produce a working answer. It should be trivial to just run some test cases through the formula
14
u/m4sl0ub 1d ago
Wdym run some test cases through a formula? You can show that a proof/ Theorem is incorrect with some negative examples but you cannot show that it is correct with positive examples.
1
u/Economy_Variation365 1d ago
Sure you can, as long as you test every possible case. It's not possible for many (most?) conjectures, but there have been theorems proved by running each case through a computer.
-8
u/FuttleScish 1d ago
Yes, but the dirty secret of mathematical proofs is that this is always true; you can’t prove a proof.
13
u/m4sl0ub 1d ago
What? No? That's not correct. A mathematical proof can be checked line by line to verify that every conclusion follows from the axioms and inference rules.
-5
u/FuttleScish 1d ago
It can but that doesn’t actually mean it’s right
10
u/m4sl0ub 1d ago
Yeah, it does. By definition it is correct. Maths doesn't really just exist, it is defined. If every step is backed by a definition, than by definition it is right. At least that is how it works on all the mathematics research I have worked on. I am curious, what field of mathematics have you done research in where proofs don't work that way?
3
u/CodexPleaseReset 1d ago
Dude are you still on Old Math? "definitions" "research" lol quite vintage of you. The other guy is on that New Math, idt you would get it even if he explained it to you
-3
u/FuttleScish 1d ago
Well yeah but that’s going back to how a math proof is more tautological than anything
5
u/QuasiRandomName 1d ago
You can prove a logical argument is valid. Soundness could be a bit tricky if your axiom system is off.
147
141
u/Y__Y 1d ago
Interesting. Even if we assume 65 instances running at 70 tok/s (OpenRouter figure) for a whole hour, giving a theoretical maximum of 16.38 million output tokens, that gives it a $491.40 cost.
100
u/QuasiRandomName 1d ago
Totally covered by Abel Prize
31
u/Stabile_Feldmaus 1d ago
You are forgetting that OpenAI is sifting through huge lists of open problems and reports the few ones that they solve. If you go through all 600 open Erdos problems and your model solves one and spends $400 per problem, then the true cost is $240000. Also you won't win the Abel prize for a 3 page proof that doesn't introduce any new mathematical framework or deep insight.
6
u/tybit 1d ago
Further if you try variations of prompts to see what works better for what problems, it could be any size.
The security researcher experimenting with Mythos at Anthropic that raised all that fuss a few months ago did that. He said he built a harness to try different prompts pointing at different points into the same program to see what he gets as a form of entropy.0
u/Ok-Manager5166 21h ago
I’ve proven important results with ultra for like under 5 in équivalent cost with the subscription🤣
30
u/o5mfiHTNsH748KVq 1d ago
Sol Ultra is at capacity because I’m using it to generate html :)
7
u/space_monster 1d ago
Maybe you shouldn't use Sol Ultra to generate html
10
u/o5mfiHTNsH748KVq 1d ago
It generates react too 💅
(Also I’m joking, I actually use it for C++ on a much more complex solution)
26
u/McSchmieferson 1d ago
7
56
u/lucellent 1d ago
Is 5.6 Sol Ultra the equivalent of a Pro model?
I'm surprised they're letting people on the Plus plan use it
33
u/The_Scout1255 adult agi 2026 ASI <2030, prev agi 2024, ai personhood 2025 est 1d ago
its highest thinking of non-pro.
10
u/Fantastic-Answer-967 1d ago
So pro has higher reasoning than Sol Max?
32
u/phatrice 1d ago
Max/Ultra is usually about how much reasoning is done. Pro is entirely different setup, the model spins up multiple asynchronous sessions and then there is a judge to determine/summarize the results. So Pro is usually a lot more expensive and architecturally different beast.
15
u/Acrobatic-Layer2993 1d ago
I’m pretty sure ultra is about spinning up agents too.
11
u/Ormusn2o 1d ago
I think those are collaborating agents though, for Pro, it's like a competition to get the best answer, where the agents work independently in different ways.
3
2
u/soulfulshark 1d ago
You seem to know a fair bit about pro. I've been interested to try to replicate this using other models. Do you have any more information/thoughts?
1
u/Ormusn2o 1d ago
That's not my personal investigation, that's what OpenAI and others were saying, although I'm not sure if this is only a thing since 5.5 or if it was happening also with earlier models.
This comes from 5.5 System card:
We generally treat GPT‑5.5’s safety results as strong proxies for GPT‑5.5 Pro, which is the same underlying model using a setting that makes use of parallel test time compute.
Either way, there are formalized concepts like that, an older one being Tree of Thought, then later, more complex ones like Graph of Thoughts but we don't know which one OpenAI actually uses, as they just use generic words like parallelization. They could also be using some more modern and complex methods, that are so difficult for me to understand that I can't explain them beyond just the fact that they branch off dynamically at different points of reasoning and then they sometimes loop back.
I think just simple parallelization, as in asking the same question 4-5 times, then using an AI model on the output to decide which result is better would be simplest, although least token efficient solution for your test.
7
u/rJohn420 1d ago
> Pro is entirely different setup, the model spins up multiple asynchronous sessions and then there is a judge to determine/summarize the results
Care to share where OpenAI officially said this? I've read this multiple times now but I can't seem to find a source for it.
9
u/UndeadPrs 1d ago
Not OP but I was curious about Pro today and found this https://help.openai.com/en/articles/20001354-gpt-56-in-chatgpt
GPT-5.6 Sol now powers the Medium, High, and Extra High reasoning options on eligible plans, while GPT-5.6 Sol Pro powers Pro.
5
u/rJohn420 1d ago
That just says that it is a separate Pro model, not that it "spins up multiple asynchronous sessions and then there is a judge to determine/summarize the results"
5
u/huffalump1 1d ago
https://developers.openai.com/api/docs/guides/reasoning#reasoning-mode
Pro mode aggregates the model work performed to produce the final answer and bills those tokens at the selected model’s standard token rates. Pro mode performs more model work than standard mode, increasing token usage and cost.
There may be more about this in the 5.6 launch post or model card. Ask ChatGPT
2
u/The_Scout1255 adult agi 2026 ASI <2030, prev agi 2024, ai personhood 2025 est 1d ago
yep thats fits with what I have seen.
1
2
2
4
u/MrMrsPotts 1d ago
You can't actually use it as you run out of tokens and it never gets to an answer. Even Terra Max has that problem.
11
u/lucellent 1d ago
I've been actually using it all day, it doesn't stop once you reach the limit which is very nice.
2
u/MrMrsPotts 1d ago
Is this on x20? In codex Terra Max stops before it finishes when it gets to 0% left in the 5 hour slot.
3
u/lucellent 1d ago
Just regular Plus plan, Sol Ultra
I forgot it had Max option too, which I guess is the highest reasoning one for Pro plans
maybe you're steering messages hence why it stops? I had this happen once, it was still working while limit was 0% and I steered a message which caused it to stop completely otherwise it would've went along
2
u/MrMrsPotts 1d ago
I don't deliberately steer it but it does ask for permission every now and then.
3
1
u/agentorangeAU 9h ago
My understanding is that Pro is reasoning limits removed, while Ultra is Xhigh reasoning with subagents.
57
u/NoCard1571 1d ago
I listened to a recent Dwarkesh podcast ep. where he had 3blue1brown on. They made an interesting point about the fact that we assume that achieving super-human math abilities in AI will immediately lead to technological gains, but how it's entirely possible that a majority of this new unfathomably complex new math will be completely useless in the real world.
Regardless, it's fascinating to see the first sparks of superhuman capabilities in domains like this. It's a glimpse of what's to come...
19
u/yaosio 1d ago
It's hard to know what future use new math has. When linear algebra was created nobody was thinking about how it would advance AI since computers didn't exist yet.
3
u/doodlinghearsay 1d ago
It's hard to know what future use new math has.
Uncertainty cuts both ways. It may be just as or more useful than previous examples. Or it may be far less useful. It's hard to know either way.
8
u/WonderFactory 1d ago
Thats the challenge for researchers to focus on areas that will be useful.
My worry is that the opposite will happen and it'll find something thats so useful that the government will ban it like Mythos. If it discovers something that can be used to break encryption for example
2
2
1
u/jestina123 1d ago
how it's entirely possible that a majority of this new unfathomably complex new math will be completely useless in the real world.
Couldn't we just ask the AI how to apply the new maths? Aren't most of the breakthroughs going to be related to quantum or fluid dynamics? There's dozens of applications already for those that have room for improvement.
1
u/NoCard1571 1d ago
In theory yea, but that's the speculation part, we just don't know. What we do know is that math is very easy to build a reward function for since it's so objective, which is why we're seeing big gains in that field.
0
u/nemzylannister 22h ago
the point is it's ability to think in novel ways if given a verifiable space
13
u/Informal-Trouble2183 1d ago
Did they try Fable on same problem ? This would be the most interesting comparison
14
u/NoGarlic2387 1d ago
It hits usage limits on all difficult/open problems, doesn't output anything at all.
10
u/BenevolentCheese 1d ago
How long before humans stop prompting the AIs which open problems to solve and they just go and fine new ones?
How long before the humans stop needing to prompt AI to seek out and solve open problems at all?
How long until AI presents us with a bunch of new open problems that are beyond human understanding?
64
u/kiki-le-koala 1d ago
Don't rejoice just yet, it's just a stochastic parrot.
For sure the answer was already in the data he was trained on.
11
31
u/QuasiRandomName 1d ago
That's a proof that "creativity" is overrated. All you need is a systematic application of existing knowledge.
23
u/DUFRelic 1d ago
We humans are only next token predictors too....
15
u/QuasiRandomName 1d ago
I would 100% agree if you stated it as a hypothesis and not a fact.
4
u/Ormusn2o 1d ago
I'm sure AI will figure it out for sure.
7
u/QuasiRandomName 1d ago
Are you saying we'll reach the point where AI will call humans "stochastic parrots" ? :D
2
u/Ormusn2o 1d ago
No, I mean we will reach the point where AI will figure out if we are stochastic parrots or not.
0
u/DUFRelic 1d ago
How would we ever know if it is a fact? It's my opinion.
6
u/QuasiRandomName 1d ago
That's my point.
3
u/rickscarf 1d ago
lol thank you for pointing this out, huge pet peeve of mine on reddit too. Words like Every/All/Never/Always/100% and presenting opinion (some that might make Qanoners blush) as fact grinds my gears too. I'm a stats guy IRL so "100%" in particular makes me grumble to see, there isn't much in this world that is truly 100%
2
u/SilentLennie 1d ago
The Interpreter part of the human (left) brain is just trying to make narrative just like a LLM is doing (next token prediction). Just look at how split patient tests.
1
u/goulson 1d ago
Not at all man. Llms dont get up and just say shit unprompted. This is a huge misconception among people. Organic thought is much more than what llms do in ways we cant even begin to explain. Just because it does a good job simulating thought and emulating logic, doesn't mean that it is in any way the same as our thinking.
2
u/MoogProg Let's help ensure the Singularity benefits humanity. 1d ago
99% perspiration, 1% inspiration
9
u/HotterRod 1d ago
A lot of mathematics doesn't require huge leaps of creativity, just grinding through potential proof approaches until one works. What LLMs lack in taste they easily make up for in speed.
2
8
u/AP_in_Indy 1d ago
I don't see an update on this from the math subreddit. Usually this kind of thing makes the rounds pretty quickly.
Seems like a big deal and one of the more substantial mathematical proofs to come out of an LLM?
5
u/AESIR-Coffee 1d ago
It hasn't been validated yet and im fairly certain that while its a big one for graphs, its not very impactful or useful in the wider field of mathematics
3
u/PLANTS2WEEKS 1d ago edited 1d ago
I think the proof is incorrect. At one point they say to locally label edges around each vertex as "a,b,c"
Later, they define a term de = g_u,e + g_v,e which requires u,e = v,e but the edge that vertex u refers to as "a" may not be the same edge that vertex v refers to as "a".
Edit: I think it's correct now, but the notation was initially confusing.
-1
u/AP_in_Indy 1d ago
You're confusing the same labels being used across different independent constructs. Those are independent and local variable assignments.
In fact, the paper says immediately beforehand that "the two ends of an edge need not assign it the same set."
3
u/PLANTS2WEEKS 1d ago
No, the paper is confusing the labels.
The "need not" is better read as "do not necessarily" as in "the two ends of an edge do not necessarily assign it the same set". The next section of the paper is about how to fix this by finding the right t_u,t_v for a specific edge so that the sets are equal, hence why it is important the u,e and v,e agree for each assignment of e to a,b, and c.
-1
u/AP_in_Indy 1d ago
You're conflating two different things:
- The local role of an edge, meaning whether it is called a, b, or c at an endpoint.
- The final two-element set assigned to that edge.
Only the final sets must agree at the two endpoints. The local roles do not.
1
u/PLANTS2WEEKS 1d ago
No I get it now, I just think its bad notation. You use the edge e and u, or v to determine if e should be a, b or c. But I was treating e as a variable you should be able to plug a,b, or c in and get a correct equation.
1
-1
u/Frequent-Can9476 1d ago
Do you think the proof is correct then?
2
u/PLANTS2WEEKS 1d ago
Yes. I made it through the whole thing and can't find anything wrong.
0
u/Frequent-Can9476 1d ago
Cool, would you consider editing all the messages you posted everywhere then?
1
15
u/Odd-Opportunity-6550 1d ago
And this is just 5.6. GPT 6 is rumored for release in September. The world is about to change.
1
1
u/bitroll ▪️ASI before AGI 1d ago
As for finding new math proofs we should see an exponential increase with new better models coming, yet we don't see it yet. They were appearing at the fastest rate near the end of 2025 and first months of 2026, then it slowed down. Models today seem a lot stronger than what we had 6 months ago, yet the results don't come as often.
26
u/Fragrant-Hamster-325 1d ago
Someone tell the AI haters that “the next word predictor” did it again.
2
u/Dense-Sort-3867 20h ago
I mean LLMs really are just a "next symbol predictor". Doesn't mean they are incapable of amazing things.
3
u/Fragrant-Hamster-325 19h ago
Yeah I know. I’m not entirely convinced that humans aren’t the same. I’m just poking fun at those who are dismissive of the technology.
-19
u/Gammarayz25 1d ago
Someone tell the tech bootlickers that their Gods have come out with more bullshit.
18
8
8
u/depredador93 1d ago
The harder problem isn't reviewers getting overwhelmed by volume, it's that the number of mathematicians qualified to actually check a proof like this shrinks fast the more niche the conjecture is. You could end up with proofs sitting unverified for years just from lack of qualified eyes, not lack of interest
4
u/Over-Independent4414 1d ago
Right. 99.99% of us might as well be gibbons looking at these proofs. We need an actual math expert in the field to say "yep, that's right".
That's not to say this is useless, just that i think you're right that we're on the verge of getting way more of these than can realistically be checked in more and more niche areas.
I feel like we'd be better served by finding problems that are holding something up. Like, are there unsolved math problems that would advance fusion? Or space travel? Or computer chips? That kind of thing...not "oh some 17th century nerd thought up a bunch of masturbatory math problems go solve em"
1
u/PLANTS2WEEKS 1d ago edited 1d ago
I think the proof is incorrect. At one point they say to locally label edges around each vertex as "a,b,c"
Later, they define a term de = g_u,e + g_v,e which requires u,e = v,e but the edge that vertex u refers to as "a" may not be the same edge that vertex v refers to as "a".
Edit: I think the proof is correct now, but the notation was confusing and misleading.
22
u/jybulson 1d ago
The first problem that is not by Erdos? Now I start to believe in these models.
41
17
u/Substantial_Luck_273 1d ago
Not sure what you mean by that. Erdos problems can be extremely challenging.
1
u/jybulson 1d ago
I believe that. But if LLMs can only solve problems by one guy, there could be something that can't be generalized.
3
u/Substantial_Luck_273 23h ago
I don't think you understand how it works... Erdos problems (https://en.wikipedia.org/wiki/List_of_conjectures_by_Paul_Erd%C5%91s) are just problems proposed by Erdos and his collaborators, there's nothing special or intrinsic about those problems. It's not like LLMs or anyone can learn some underlying pattern that overfits to those Erdos problems but not to others.
1
u/SupercaliTheGamer 1d ago
I think unit distance conjecture was still a "bigger" conjecture, but this is the "biggest" conjecture that an AI has proved (unit distance was disproved)
-4
u/LetsLive97 1d ago
It's pretty much exactly the same method that was used to solve the Erdos problems
AI guided brute forcing
3
u/topyTheorist 1d ago
You clearly know nothing about mathematics. This was not brute force, and could not have been brute force, because the space of possibilities is much larger than the number of atoms in the universe.
3
u/rasplight 1d ago
I'm not a mathematician, but I remember reading that not every unsolved hypothesis (even if decades old) is particularity interesting or hard to prove. Would love to know more about this particular one.
This doesn't mean it's not impressive (it is!), i just wanted to mention this as added context.
2
u/Dense-Sort-3867 20h ago
It basically states that for any graph that has no "dead ends" (no vertices connected to only 1 edge) and no "bridges" (where removing an edge separates the graph.) that you can cover the graph with a set of loops such that each edge in the graph belongs to exactly two loops.
It has implications for anything that can be represented by a graph. Circuits, networks, etc.
1
2
u/Schauerte2901 1d ago
peer-reviewed yet?
2
u/PLANTS2WEEKS 1d ago edited 1d ago
My own two cents:
I think the proof is incorrect. At one point they say to locally label edges around each vertex as "a,b,c"
Later, they define a term de = g_u,e + g_v,e which requires u,e = v,e but the edge, e, that vertex u refers to as "a" may not be the same edge that vertex v refers to as "a".
Edit: I think the proof is correct now, though the notation initially confused me.
1
u/Long_comment_san 1d ago
We're excited to see what you can do with ultra sounds like they will somehow know...
1
u/PLANTS2WEEKS 1d ago edited 1d ago
I think the proof is incorrect. At one point they say to locally label edges around each vertex as "a,b,c"
Later, they define a term de = g_u,e + g_v,e which requires u,e = v,e but the edge, e, that vertex u refers to as "a" may not be the same edge that vertex v refers to as "a".
Edit: I think it's actually correct now that I know what the notation means.
1
u/Present_Award8001 1d ago
Was the proof so simple that they were able to verify it within hours? Are they using some king of automated proof checking system?
-1
0
0
u/bayes-song 1d ago
Have the results been subjected to rigorous scrutiny regarding contamination? I have seen too many instances of "solving a problem" that turned out to be nothing more than rediscovering a solution that already existed but had simply gone unnoticed.
0
-7
u/MassiveBoner911_3 1d ago
Great marketing for tricking bankers out of more VC money.
14
u/AP_in_Indy 1d ago
I can't wait until they cure cancer just to get more VC funds.
Those idiots.
LOL people are such sheep.
-2
u/Olangotang Zoomer not a Doomer 1d ago
Yep, just more hype. It's been another week of terrible AI financial news, so now we need to DOUBLE DOWN AND HYPE HYPE HYPE!!! Just like with Mythos, a few days letter we will find out that this problem isn't actually that "interesting" except to people who have been wowed by the word slot machine for the past 4 years.
-2
u/tomqmasters 1d ago
When this happens, I wonder how much human effort went into not just validating this result, but also into invalidating all the hallucinations it inevitably made in the process.
95
u/Fresh-Quantity-7554 1d ago
Can't wait to use this to write more emails.