my guess is that probably these problems aren’t that well known to the general public? unlike Navier-Stokes, etc.

if the likes of Riemann Hypothesis, P vs NP, etc. got proven i bet everyone will hear about it immediately.

Saying “self-verified” is massively downplaying it. They are formalized and checked in Lean4 1, which is a programming language used by mathematicians today, to mechanically check their proofs to rule out human error. In other words a theory being stated in Lean generally means it’s more likely to be correct than one stated in mere human language.

Now, Lean, like any piece of software, has had bugs. A while back someone exploited a Lean bug to “prove” the Collatz conjecture 2. So it is possible that AI agents found a bug and used it. But the vibes I got from mathematicians in the field is that that’s not very likely.

• L=RL=BPL
• multiplying two numbers can be faster than nlogn
• matrix multiplication in n^2.25
• 3sum is subquadratic
• Hilbert tenth problem over rationals
• Unique game conjecture - now theorem

To name but a few. Each of these alone can be ground breaking.

Edit: sorry, the 3sum result was not from this batch. it happened around the same time so it got jumbled in my brain, but this one was proved by Claude.

At least half of these are formally verified. Although they did retract 3 papers. Out of about 700

we are going to give clanker rights before we have trans rights 💀

I do not want to appear like I want to defend them because I don’t.

Your understanding of what they did is not correct. But also fuck OpenAI I am not going to explain their bullshit for them. So anyway put Sam Altman in prison is all I am going to say.

no… AI companies targeted US and Canadian government websites.

Have you ever put all your Sims in the swimming pool and remove the ladder?

I remember people were trying to call it confabulation which is still anthropomorphic and it didn’t catch on

A lot of the suggestions there are confusing and/or unhelpful

Like

hallucination → undesirable output

We all know what AI hallucinations are, calling it “undesired output” just removes all the specificity and makes communication more difficult.