YHK - yet another hacker news clone

Working with academic communities to build scientific understanding

253 points jonluca 2 hours ago 112 comments

rbranson 2 hours ago | parent

The title buries the lede quite a bit:

> The Exponential Time Hypothesis is false

krackers 2 hours ago | parent

https://github.com/openai/math/tree/main/preprints/The-Expon...

>We give a deterministic algorithm for exactly counting the satisfying assignments of an arbitrary k-CNF formula [in superpolynomial but subexponential time]

baq 1 hour ago | parent

What a time to be alive honestly. Can’t know what one will wake up to

adverbly 54 minutes ago | parent

> superpolynomial

I've got some reading to do it seems...

JonChesterfield 2 hours ago | parent

https://github.com/openai/math/blob/main/lean/docs/378.md

JonChesterfield 2 hours ago | parent

by fucking sorry written at the end of the proof

mattr03 1 hour ago | parent

https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050...

looks like the real proof is in this file

JonChesterfield 1 hour ago | parent

awesome, thanks!

sebzim4500 1 hour ago | parent

They do that to make it easier for readers to verify the statement (which is entirely contained in that file) separately from the proof (which is spread over thousands of files and github can't even show them all).

Proof is at https://github.com/openai/math/tree/main/lean/OAI/Algorithms...

ollin 1 hour ago | parent

I was confused too, but it looks like https://github.com/openai/math/blob/main/lean/ComparatorChal... (with the sorry at the end) is just the problem statement; the actual proof is a big pile of lean in the Algorithms folder, with the final theorem stated here https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050...

Sniffnoy 2 hours ago | parent

This is just one of the three ledes, really!

yu3zhou4 1 hour ago | parent

A newbie here, does it mean that SETH is false too?

pavitheran 1 hour ago | parent

Yes it means both SETH and ETH are false.

levocardia 1 hour ago | parent

Oh and also:

>Our models produced a natural language proof for Yang–Mills existence on September 9th, 2026

And presumably they are just missing the "mass gap" part of it.

Very clearly these were the results of taking big swings at all millenium prize problems.

mlinsey 2 hours ago | parent

I understand that the Exponential Time Hypothesis being false doesn't necessarily mean P=NP, but for people who are a lot more knowledgeable about complexity theory, does this update your priors significantly in the direction of P=NP?

novaRom 1 hour ago | parent

For me, this result is significant. It basically adds much more hope P is equal NP (that majority seems being against). I believe one day AI will explain a major flaw in modern mathematics, so a kind of correction in axioms will be suggested to prove Rieman's hypothesis (or a completely new apparatus)

rcpt 1 hour ago | parent

I don't know if that's a "flaw". It's what Godel Incompleteness guarantees.

Would be funny if the most famous problem turns out be an example though

skew-aberration 1 hour ago | parent

That's not that how that works btw. The incompleteness is a property of the algorithm which does the proofs, not the theorems. If a theorem is true it has a proof and a program which proves it (printf("the proof verbatim")). But no computer program can successfully prove all theorems. The space of potential proofs is too big to search systematically, but you can still get lucky.

rcpt 30 minutes ago | parent

Godel says that there are statements that are true but have no proof within that system. It's not about algorithms.

I'm saying it'd be funny if Riemann were true but not proveable.

Though I guess it's actually funnier. If Riemann were false then there would be a counterexample, so it's clearly within existing axioms.

So if one can prove that Riemann isn't proveable in our current axioms then it has to be true.

noslenwerdna 19 minutes ago | parent

That is also not how it works. The theorem says that there exist some true statements for which there is no proof. This is assuming the axioms are consistent.

_dain_ 27 minutes ago | parent

Why do you "hope" P=NP? It would be a catastrophe

varjag 1 hour ago | parent

Imagine you're trying to prove that water is wet (P!=NP). You lack a formalism that could make sense at building a proof even though pretty much everyone agrees from empirical evidence that the water is indeed wet. A promising attempt at building one such formalism was just demonstrated by a model to be a dead end.

jaaron 25 minutes ago | parent

I like this, but the actual finding is a bit different. Trying to keep the water is wet makes this awkward, but I believe it's more like:

Everyone agrees that water is wet (P!=NP), but no one can prove it. In the meantime, a whole field of computer science was built on a stronger belief (ETH): that water, at its worst, soaks. Turns out, even at its worst, water only makes things damp. It's still wet. That said, this finding did produce a new measurement of wetness.

jltsiren 13 minutes ago | parent

It's been a long time since I seriously thought about complexity theory, but I'd say no. For similar reasons to why complexity class E is not closed under polynomial-time reductions.

The most important component in the time bound is of the form 2^{n / polylog(n)}, which is subexponential. But if you have reduction from another problem that increases instance size quadratically, the algorithm for the other problem is no longer subexponential. Which means we are still essentially in the same neighborhood as before.

It's a huge result if true, and probably the first major AI result that affects the papers I read. But since the boundary in the hypothesis was kind of arbitrary, breaching it should not significantly change our intuition on complexity classes.

calf 2 hours ago | parent

In the Star Trek Voyager capstone episodes titled "Scorpion" parts 1 & 2, Chakotay explains to Janeway the behavior of the Borg through the parable of the fox and the scorpion making a transactional deal to cross the river together. After reaching the shore, the scorpion stings the fox, and the dying fox asks why. The scorpion replies, "Because it is in my nature."

(Upside of the story is Captain Janeway's trusted crew works together to formulate a trick up their sleeve precisely in case of predicted contingency...)

mudita 1 hour ago | parent

The fable of the scorpion and the frog is not original to Star Trek.

https://en.wikipedia.org/wiki/The_Scorpion_and_the_Frog

paxy 2 hours ago | parent

Title is no doubt crafted to get ahead of the usual online backlash, but here’s the actual announcement:

> We are announcing three new discoveries in mathematics, computer science, and physics about harmonic analysis, complexity theory, and quantum field theory.

1. Local smoothing and the Kakeya conjecture

2. The Exponential Time Hypothesis is false

3. Existence of quantum chromodynamics and completions of the Standard Model

Rudybega 1 hour ago | parent

To give some context:

Kakeya / local smoothing (math): The result would resolve the Kakeya conjecture and Stein’s restriction conjecture across all dimensions together. Mathematicians had been making progress one dimension at a time, so this would settle a whole family of central harmonic analysis problems at once.

ETH is false (computer science): ETH has been used as a computational hardness premise in hundreds of papers, so a disproof would undercut a large body of existing complexity results. It would also change what researchers think is achievable for efficient computation.

QCD existence (physics): It would give a rigorous mathematical foundation to the theory of the strong force, which physicists have used for decades without proving it’s well-defined. It also bears on a Millennium Prize Problem.

jlev1 1 hour ago | parent

Thanks Claude!

Rudybega 43 minutes ago | parent

Glad to help (I only really understand the implications of ETH well enough to summarize myself without assistance haha). I figured if I wanted simplified context, others might too.

emil-lp 1 hour ago | parent

I would guess ETH has been assumed in thousands of papers. I have several myself.

On the positive side, suddenly there's a whole bunch of open problems!

dekhn 1 hour ago | parent

Is there any obvious path from these results to any sort of physics, chemistry, or biology breakthrough? From what I can tell: no (but I lack the physics and chemistry expertise to say anything about the QCD finding).

Turning the question arouhnd: what would be the most impactful thing for OpenAI or Anthropic to do to show large breakthroughs?

demibabs 55 minutes ago | parent

Solve p = np with an example algorithm maybe?

Kotlopou 51 minutes ago | parent

From the physics, not without more breakthroughs, and even then I can't imagine what that would look like. The particle physics that you can use industrially has long been understood, and the field has long been long stuck because the only things we don't understand are also insanely expensive to experimentally access. Maybe once we move up the Kardashev scale, though.

ETH sounds more like there's a path it could become important? In general, the recent complexity results suggest that a) our intuitions about that world are unreliable, and b) the truth seems to be insanely complicated. I mean, new faster multiplication algorithms in 2026, what the hell? How can we say anything about the full space of all possible algorithms?

redox99 33 minutes ago | parent

If we had really good understanding of physics, couldn't we find out how to make a room temperature superconductor (or prove it can't exist)?

Or is such understanding reliant in experimentation because there are "hidden constants" we can't figure out with math alone?

abetusk 28 minutes ago | parent

ETH is false! I really would not have believed it.

[0]:

> We give a deterministic algorithm for exactly counting the satisfying assignments of an arbitrary k-CNF formula. For every fixed k ⩾ 2, on a formula with n variables and m clauses, our algorithm uses $poly_k (n, m)$ space and runs in time $(n + m)^{O_k(1)} 2^{n/(\log n)^{1/2 + o(1)}}$

The dominant term there is (roughly) $2^{n / (\log n)^{0.5}}$, so still superpolynomial but less than exponential. Fucking wild.

[0] https://github.com/openai/math/blob/main/preprints/The-Expon...

esalman 2 hours ago | parent

Working with academic communities lol.

I looked over the announcement for any substantial contribution, and found they're donating $5 million to a research foundation.

$5 million might sustain 5-10 PhD students for 5 years.

Maybe it's just me but I think they should contribute more in exchange for forcing the scientific community into paying for tokens to generate slop and then pouring their time into verifying or falsifying the slop.

quantumspandex 1 hour ago | parent

No one "forces" anyone to verify it.

LPisGood 1 hour ago | parent

I said the same thing in another thread and someone compared it to no one forcing you to own a smart phone. I will preempt that argument by saying the community is motivated to verify these results because they are important to the field.

esalman 28 minutes ago | parent

That means there's no crisis in mathematics after all, right?

dooglius 1 hour ago | parent

The proof appears to be a sub-exponential algorithm for #3-SAT not just 3-SAT, I think this is considered a much stronger result?

geysersam 1 hour ago | parent

Isn't 3-SAT NP-complete?

LPisGood 1 hour ago | parent

It is the canonical NP complete problem.

krackers 1 hour ago | parent

Yes. Up until now, it was unknown whether containment of NP in EXPTIME was strict or not. (Obviously you can brute-force all possible witnesses, so any problem in NP can be solved in EXPTIME, it was open whether you could do better than that.)

Showing 3SAT (technically #3SAT) can be solved in less than EXPTIME resolves this. It's only slightly subexponential, not even quasipolynomial, but it is a very surprising result. And that too a constructive algorithm.

Edit: Apparently not true, the constructive algorithm given may not survive under reductions. See discussion in https://news.ycombinator.com/item?id=50251661

3abiton 1 hour ago | parent

I am not sure if I side with Tao on this, or 3B1B. It's already causing quite a kerfuffle (to say the least) in the academic communities. This is the new norm now.

mentalgear 1 hour ago | parent

"Working with PR to make us look less like cheating mind leeches".

artninja1988 1 hour ago | parent

I wonder how much compute they are throwing at problems in ML like continual learning and sample efficiency. Also how successful they are with these. Results like in the post make me hopeful we'll see some type of so singularity soon

titzer 1 hour ago | parent

I'm going to be the cynical one and offer this translation: "Our results are too important to wait for the pesky peer review, so we are dumping a whole ton of money in a fund and giving some elites a breathless first look so our buzz keeps getting jacked up."

The reality that Science is a grind and there are thousands of new results every year discovered by regular humans who use a regular human process to cross-check and review.

Treating every result from the AI like a gift from god is getting tiring.

quantumspandex 1 hour ago | parent

Science doesn't have to be a grind with AI.

sgillen 1 hour ago | parent

These are not run of the mill results from AI, those are surely being posted to arxiv constantly by normal researchers without any fanfare.

These are really big results from AI, if a human had come up with them we would also be making a really big deal out of them too (maybe not as big of a deal, part of the excitement is that this was from AI and more results of this magnitude may soon follow).

metalsiliconYT 1 hour ago | parent

OpenAi needs to stop trying to please everyone. Just release the findings and give all the credit to your models/collaborators.

sebzim4500 1 hour ago | parent

They have released them, they are just also hiring mathematicians to clean them up in parallel.

T-A 1 hour ago | parent

We reached out to external experts and asked them to act as shepherds, organizing groups to understand the new results. They advised three different release strategies: [...] For the physics result, form an external group of collaborators and defer to them on the release of materials. [...] The group requests that all communications with any and all members of the group regarding this effort be directed to the following email account: YANGMILLS4D@gmail.com.

karmasimida 1 hour ago | parent

Well, they are also not fully sure they got it right.

1ahsgt 1 hour ago | parent

I wonder how many prompts for proof approaches they stole for these. Nothing on how many tokens were burned.

Proud to funnel money through the Simons Foundation, which is an AI booster itself and completely aligned with OpenAI.

They make it very hard to enjoy a single result with the business and the politics being so dirty.

jwpapi 1 hour ago | parent

Honestly, I’m a bit scared but also a bit excited.

I’m currently reading Africa by John Reader which covers a lot of humanity storyline. From HN I get the humanity achievements that are happening right now.

The feeling digesting both daily is in order of magnitudes bigger than what any really exciting tv show did to me.

I honestly at this point don’t know anything about what could be possible and what couldnt.

I understand that this is really freightening, but also especially ETH being false gives even more hope that some fundamental problems could be solved in our lifetime, for example understanding universe, aging, colonization of planets and also our limits. I know I’m the minority, but these answers really interest me.

kypro 1 hour ago | parent

> gives even more hope that some fundamental problems could be solved in our lifetime, for example understanding universe, aging, colonization of planets and also our limits.

There are infinitely many more ways to kill and torture a human than to save one.

adverbly 51 minutes ago | parent

Wrong. There are infinite ways of doing both.

jwpapi 45 minutes ago | parent

I honestly think they are both finite lol.

adverbly 36 minutes ago | parent

Maybe.

Depends on what counts as a different way I guess.

And on if you're applying some kind of discrete physical model of the world or not...

dekhn 1 hour ago | parent

Nobody is solving colonization of planets in this lifetime unless we find a way to accelerate mass faster than the speed of light (and decelerate it at the other end) or extend the lifespan/radiation resistance or can preserve bodies in suspended animation for long periods. Even then, that just removed one of the many technical hurdles. We don't know which planets to target- are you going to send people to solar systems when you don't know if they are habitable? Modify people to be able to inhabit otherwise hostile worlds? How do you deal with boredom on a 1,000+ year trip?

Even with aging, our efforts are better spent increasing quality of life across humanity than helping a few rich people live to 150.

jwpapi 54 minutes ago | parent

How about sending robots to a habitable planet with biological material of humans, programmed to tell us the story of earth?

Re life quality: Sure technical advancement can lead to cheaper electricity, better materials discovered, disease prevention and a lot of other stuff. A lot is hold back by complexity.

I don’t want to make a call that this will happen and that it’s a net-positive for society. I’m just saying the technical advancements is interesting and enablin.

hei-lima 1 hour ago | parent

Terrible title. I was hoping to see more interesting comments on the story, haha!

mindwok 1 hour ago | parent

It is mind blowing that these long-standing conjectures and open questions are just falling by the dozen every other week. What a time to be alive.

__MatrixMan__ 1 hour ago | parent

Chasing open questions, it seems to me, is worthwhile for the things learned along the way. Do you expect these results will be helpful, or is it just a sign that we need a new way to navigate uncharted spaces now that longstanding problems don't stand long enough for us to organize around?

It feels a bit like having "visited" a place because you had a layover there.

brap 50 minutes ago | parent

If knowing the answer is not valuable then asking the question wasn’t valuable to begin with.

We should remember that math exists primarily to serve a purpose and that purpose is not being a fun puzzle hobby for a select few mathematicians.

Imagine a programmer telling their boss it’s not about working software it’s about the journey of writing the code. Good luck getting hired.

I think if pro mathematicians don’t change their tune quickly they will soon see their funding approach zero.

Kotlopou 47 minutes ago | parent

I don't understand this dialogue, which seems to repeat with every result of this sort. Of course this is interesting! And of course the answer tells us something! And of course we also want to understand where it came from! None of this is in contradiction!

unknownian 34 minutes ago | parent

If you were a math grad student, would you rather your advisor be telling you to LLM maxx your ideas or working with you and giving you ideas on your thesis personally? I know my answer.

brap 12 minutes ago | parent

To say that we must have people that know how to X, because otherwise no one will be able to teach how to X, is kind of circular reasoning. Why is X important to begin with? What’s its inherent value to society?

cman1444 50 minutes ago | parent

I hope it's more like discovering islands of information which we can use as footholds to connect the dots between them.

ChemSpider 57 minutes ago | parent

How long until we see similar announcements for (wet lab) chemistry, medicine or material science? Months? Years? Never?

(Never would mean AI will be used in future labs like a fancy calculator, but not much more changes)

dannykwells 42 minutes ago | parent

Well you can’t verify a prediction about human biology without a phase 3 clinical trial so…

Routine8502 37 minutes ago | parent

I'll give you an example from my field (nuclear fusion). I have a small team working on an idea which I think would really advance the field. Our initial concept paper was published in 2019. Progress on it has been slow because we don't have enough manufacturing capabilities, budget, or time on the facility. Will AI solve that? Don't get me wrong, I'm pretty bullish on AI, and it's been phenomenally useful so far (I definitely feel like a 10x physicist in the last 6 months), but I don't see a swarm of agents putting fusion energy on the grid tomorrow.

Also, fwiw I have a personal test problem I give to every frontier model on release, which is to ask it to final a realatively obvious solution (in hindsight) to a minorly important open problem in my field. I know the answer, but havent gotten around to writing it up yet (it's really not that important). Every frontier model (so far) just regurgitates existing solutions.

szvsw 27 minutes ago | parent

How much effort do you put into prompting it? Are you asking it one shot with a simple prompt? Are you giving it to multiple agents and giving them a workspace to collaborate in? You might give it to a trusted colleague who does not know the solution along with an agreement to jointly publish, ask them to go through the process of solving it with agentic support, and then compare your solutions.

Edit: to be clear, I completely believe your experience - just pointing out that it might be interesting for you to actually “try” to solve it thoroughly with the tools, though it is obviously hard to do that in a fair way when you know the solution.

marshray 26 minutes ago | parent

Definitely. It will let some smooth-talker with a vibe-coded website raise billions for "Nuclear Fusion AI". Then they can use AI to squeeze your team with lawsuits until you agree to sell cheap, and maybe keep you on as an employee to build it.

wilg 1 hour ago | parent

In my opinion its okay for them to work on science and math problems and release the results.

ATMLOTTOBEER 43 minutes ago | parent

Thanks, I work at oai and will relay your approval to my line manager

aborsy 1 hour ago | parent

Science is getting out of the reach of the majority of people. In particular, EU is out of it mostly.

rcr-anti 1 hour ago | parent

Well, this is certainly different, can't say they ignored the criticism. Wonder if this is a monkey paw curls moment; if the findings continue to accelerate, most of it just isn't public now.

Daniel_Van_Zant 1 hour ago | parent

Lots of progress recently in formally verifiable domains. Really curious if this is a product of the machine learning folks behind most large language models being much more likely to have a background in math, physics, etc. Or if it is that large language models have some fundamental limitations in the more "scruffy" sciences like biology.

My guess is that in formally verifiable domains you can use RL-esque processes to get lots of good high-quality training data with reward signals (does it verify?), but the same does not apply to "scruffier" work. I would also imagine that the data volume of high-quality scientific work in "scruffy" domains is too low for the large language models to have a good manifold for "high-quality biology research". Would love to be proven wrong if anyone knows of anyone doing great scientific work with large language models in non-verifiable domains though.

rcpt 1 hour ago | parent

It's the limitations for sure.

AI has dominion over the digital world, when it can verify things in Lean it's able to crush problems like they're a game of Go.

But when the real world and digital world don't quite connect AI is bottlenecked.

crabmusket 50 minutes ago | parent

Does this imply a forthcoming wet lab boom comparable to the data centre boom?

Creamsicle47 1 hour ago | parent

It's because LLMs provide an efficient way of optimizing a complex, non-linear search space when there's a way to measure progress. The less verifiable something becomes, the harder it is to optimize (but not impossible).

serioussecurity 59 minutes ago | parent

It's not just RL.

Many of the harnesses used to search for solutions rely on quick/cheap correctness checks to discard incorrect hypotheses. With something like biology, you might need to run a wet lab experiment to reject an idea. This can add days per iteration, slowing progress down by a factor of 100 or more.

The sad reality is that many computational approximations for biological phenomenon are relatively weak and lack the predictive power we need.

Frost1x 48 minutes ago | parent

I suspect the line forward is generating improved predictive models and implementations of those. It’s something LLMs can aide with, although they’ll have slower progress than domains that do already have robust, cheap validation checks. That’s probably why those domains are being targeted (they are the paths of least resistance to successes, which is why they’re being pursued).

With that said part of the reason some domains may not have robust cheap verifiers is because they’re difficult to produce already, so it may be a bigger lift.

szvsw 33 minutes ago | parent

Is there a path where compute gets poured into developing, and then eventually using, computational models that supersede the shortcoming of the existing computational approximations you mention, which thus makes computational analysis and developments possible at rapid scale?

In an area I am more familiar with though still not my domain: when the stiffness matrix and computational linear algebra methods collide, it unlocks a world of computational structural design and analysis by commoditizing the underlying mathematics. This is a simple example, but you get the idea.

Obviously with CFD, mechanics, etc there is always massive work being done to try to unlock new computational methods, faster/parallelizable computational methods, differentiable ones, etc etc, but the general feeling is that the core physics are well modeled (NS millennium problem not withstanding) and are not lacking in predictive power for useful applications. I would have assumed that the same would be generally true for computational biology etc, so just curious to hear you elaborate more. It seems plausible to me that turning the brute force of “the models” (as in, swarms of AI compute) to work on/develop/solve/address whatever representational problems there are in the computational approximations/numerical methods you mention, particularly if that is a bottleneck to performing more extensive methodological/experimental exploration in silico to enable better exploitation/use of limited resources in wet lab.

Again, I know nothing about computational biology, just stating my intuition and curious what your take is. Probably the limits of my knowledge can be demonstrated by the fact that the only modeling methods that come to mind as being vaguely relevant would be, like,… molecular dynamics, maybe discrete element method in a weird way but doubtful, and various pop science understandings of protein folding etc.

kypro 45 minutes ago | parent

Knowledge is surprisingly transferable.

Obviously it's easy to understand why having strong abilities in maths and coding can help with solving problems in physics. But it's also true of knowledge and mental models more broadly.

For example, say somehow you managed to train a frontier model without any data about elephants. If you did this it would be relatively easy to later train elephants into the weights. You'd basically just need to train it about elephants at a very superficial level. After all, it it already knows what a mammal is. It knows what legs are. It knows what eyes are. It understands how it's digestive system works. All the things that makes the biology of elephants difficult doesn't need to be learnt from scratch.

I assure you people on HN will be surprised at how quickly frontier models will become competent in domains that are harder to RL. They won't need anywhere near as much data as people currently believe.

Kotlopou 40 minutes ago | parent

Has anyone done an experiment like this? Do you have any papers to link to? This sounds quite important!

Kotlopou 1 hour ago | parent

"In our view, these manuscripts are best understood as a form of raw research data."

They are staying on top of the exact formulations that spread like memes. I think this one was unfortunate. It's an analogy for a new type of thing that stops attempts to figure out what thing that is.

That said, uh, let's go? Let's see if OpenAI earns some goodwill here. It probably can't go worse than the last math drop!

vatsachak 9 minutes ago | parent

It is raw research data though. Human math is way more refined. LLMs are superhuman at deduction, yet cannot create their own pre-training (where most learning happens) data.

adverbly 1 hour ago | parent

> In our view, these manuscripts are best understood as a form of raw research data.

Much better!

> For the computer science collaboration, the group has decided to make the natural language proof and Lean formalization public immediately, and we are publishing them directly to our GitHub repository. For the physics collaboration, the group has decided to hold off on releasing the AI-produced artifacts and instead work on writing it up themselves.

> All of these approaches involve tradeoffs. On the one hand, the collaborations empower experts to foster unpacking the results and contextualizing them in the broader academic community. On the other hand, choosing initial shepherds necessarily shapes who gets involved first and creates asymmetry of information. We welcome feedback on how to broaden participation and make this process more useful.

Very good!

I was highly critical of their approach with the earlier mathematical publications, but this is much improved.

Most importantly, they aren't releasing slop papers that would never have been published in any self-respecting journal or made it past a deep round of peer review questioning.

> We are committed to ensuring funding for researchers to independently examine, explain, and build on the results above.

> We continue to invite feedback on the best way to disclose results and engage with scientists to accelerate discovery.

Well done!

Now you need to actually LISTEN to the community and the feedback, so you aren't done yet, but this is a much better start than last time. Keep it up!

lukeplato 1 hour ago | parent

> Our models produced a natural language proof for Yang–Mills existence on September 9th, 2026, and then subsequently produced a proof for QCD on September 18th, 2026. Given the length and complexity of the work, we postponed release until the Lean formalization completed. We finished our formalization of Yang–Mills’ existence on October 16th, 2026, which led us to develop the collaboration described here

absolutely insane

doctoboggan 1 hour ago | parent

I wonder why the physicists are the only group to not want the full information released upfront? As a casual fan of physics[0] it seems like their completion of the standard model is possibly the biggest deal of all these breakthroughs, am I wrong?

[0]: PBS space time watcher

Kotlopou 58 minutes ago | parent

Careful, completion of the standard model ≠ theory of quantum gravity or theory of everything. The actual question is too abstruse for me (biophysicist).

T-A 28 minutes ago | parent

The writing is a bit ambiguous, but if I'm parsing it correctly it's only a big deal to the small subset of physicists who care about mathematical rigor: proof that Quantum Field Theory (i.e. what theorists have been using since the 1940s or so) is mathematically sound.

This part,

The existence proof pertains to the simplest grand unified theory that includes the gauge fields and fermions of the Standard Model

looks like a reference to SU(5) GUT from 1974:

https://en.wikipedia.org/wiki/Georgi%E2%80%93Glashow_model

martinhath 1 hour ago | parent

ETH is false! This is one of the big long-standing hypotheses that I actually remember from university, and afaik, it was reasonable to assume it would be true; reasonable enough for a lot of papers and results to assume this for bounds or hardness proofs of common problems in parameterized complexity, anyways.

Also glad to see that one of the authors of the paper stating it is also in the loop here.

2026 is weird.

Kotlopou 1 hour ago | parent

Regarding Yang-Mills, as of a few weeks ago there has been some expectation that this (specifically completing Balaban's program for the existence part without the mass gap) could happen, though from the Anthropic side: https://nitter.meowing.monster/ElliotGlazer/status/211115394...

(Elliot Glazer seems in general to be a pretty good source to follow, however he does that...)

Kotlopou 42 minutes ago | parent

Here (https://nitter.meowing.monster/ElliotGlazer/status/210765080...), from October 7, maybe this will be relevant soon:

> I occasionally talk to experts on all the MP's. Their rough summaries on what is needed to solve them usually go:

> Hodge: not a clue

> BSD: not a clue

> RH: not a clue

> P vs NP: not a clue

> Yang-Mills: "Well..."

Insimwytim 53 minutes ago | parent

Wow, math PR really took over, nevermind blowback from those pesky mathematicians.

Let's throw in more of that stuff, so they wouldn't look at the financials.

stabbles 48 minutes ago | parent

> In our view, these manuscripts are best understood as a form of raw research data. To convert this raw research data into scientific understanding, in this release we are experimenting with a new approach

Mathematics and computer science are turning into an empirical science

dannykwells 41 minutes ago | parent

Except that lean verification means that you really need to just verify the lean problem statement right?

nixonaddiction 35 minutes ago | parent

this is the first time one of the big labs has published anything related to my field. and i'm actually pretty excited? im more on the applications side of QFD than the theory side of things, but gosh i actually cant wait for the results to be released to see if i can use it for anything! i kinda hope more results come out, in more ways relevant to what i do, its so cool to see any sort of progress! wow!

measurablefunc 28 minutes ago | parent

Someone should take the sub-exponential proof & write something executable.

zone411 11 minutes ago | parent

These resolve 6 entries in my top 500 open problems list (LLM ranked, https://www.proofatlas.ai/open-problems/) and there is partial progress on #3 overall (Yang–Mills Existence and Mass Gap):

Kakeya conjecture — #38

Fourier restriction conjecture — #46

Local smoothing for wave equations — #187

Bochner–Riesz conjecture — #190

Exponential Time Hypothesis — #43

Strong Exponential Time Hypothesis — #63

vatsachak 8 minutes ago | parent

The proof of the Kakeya conjecture is amazing. Only 54 pages. Will probably lead to a lot of theory.

As a non abelian harmonic analysis PhD I am very happy