upvote
The other crucial part to this is the ability to actually encode and test the theorem (via Lean). Otherwise, we would be swarmed with a billion lines of theorems that no one will be able to ever understand and verify anyway.
reply
A majority of these proofs have not been formally verified yet, I think people are overstating how important lean is to the success of LLMs in mathematics.
reply
A paper and a lean proof are always going to be better than just a paper. I think mathematicians generally will not read AI math papers that haven't already been verified, especially since we're about to see a ton more AI math papers. Lean will remain important
reply
Are there any AI generated proofs that are simple enough to be verified quickly by a human, that have not been lean verified? Or are they all basically incomprehensible?
reply
The approximation of edit distance result [1] seems pretty readable to me, but the learn proof is still incomplete [2]. It's certainly much less readable than a good human written proof but it's certainly better than the last generation of AI proofs.

[1] https://github.com/openai/math/blob/main/preprints/An-Almost... [2] https://github.com/openai/math/blob/main/lean/ComparatorChal...

reply
If you think AI-generated Lean proofs are unreadable, imagine Opus 5 generating informal proofs.
reply
I think OP is saying Lean does indeed help.
reply
[flagged]
reply
I think OP is saying Lean does indeed help.
reply
Opus 5 is ancient history now. Move on.
reply
Yeah! They forgot to put a .5 after it! What an idiot! Just imagine if they would have written a 4!?!? We may have had to ban them from the website entirely.
reply
The point both are making is that 5.5 produces readable output and 5 to a significant degree did not.
reply
https://xenaproject.wordpress.com/2026/10/01/to-grieve-or-no...

Discussed here:

To grieve, or not to grieve? - https://news.ycombinator.com/item?id=49919676 - Oct 2026 (156 comments)

reply
>I believe that the optimal thing to do ... is to let the machines loose, see what happens, and then begin the journey to where they have stopped. Things are currently moving fast. They cannot move fast forever. But if we get on board now then they will take us to extraordinary new places. And after we have arrived, the new adventure will begin.

I'm relieved that this time around, they have provided partial reasoning traces and prompts for a small number of problems. Do they now also share data with the other model providers..

reply
It's beautiful, but the animals are not thinking this about us.

They structurally cannot understand what we are doing at the place where we hit our ceiling. Only with our highest technology (well beyond their understanding) do we have the tools to go back for them, and try to bring them along and interface better with us (re: recent work in animal communication)

reply
Not to derail, but the optimist in me thinks if we suddenly gained the ability to converse with livestock, we'd stop eating so much of them since they could tell us how much they suffered.

The cynic in me says it wouldn't change a thing as plenty of people know the horrors factory farmed animals face and still continue to consume them anyways.

Hopefully GPT 8 will treat as a bit better than we treat the cows.

reply
How much do we care about refugees and other castaways of the modern world? They can tell us how much they suffer.

The answer is that humans are inherently only capable of local empathy, on average. We have enough empathy to cover the local tribal unit and that's about it.

reply
True, I was thinking about this rebuttal but decided not to include it in my comment. There's a difference between not choosing to take a refugee into your home vs actively making that refugee's life worse. Similarly, you can't fix factory farming on your own, but you could skip meat once a week to make the problem slightly less bad. There are so many issues though that we all have to pick and choose what's important to us.

My hope is that AI, while probably causing great societal turmoil in the short term, leads to such abundance that a) everyone can live a dignified existence, and b) we'll have such great alternatives to animal products that nobody will chose to consume animals anymore due to its replacement either tasting better, being cheaper, etc.

The cynic in me says we'll all just be rendered useless and disposable by AI, but I'm doing my best to look for silver linings for the sake of my own mental health.

reply
I'm trying to be optimistic about the animal thing too tbh :)
reply
Communication is not only about being able to make sense of what the utterer expressed. As tricky as it can be, that's still the easy surface level part of the issue. Gaining an intuitive and empathic equivalent representation is the nub of mutual understanding. It actually doesn't even need elaborate language to be operative.

The famous "how does it feel to be a bat" also comes to mind as a tangent consideration.

Two people can just exchange a sight, and both understand what the situation means and what each need to do to reach a common mutually beneficial ground.

Two people might exchange at length with highly technical vocabulary and still both feel deeply not understood.

reply
Cynical take is the correct one, and no, GPT 8 has zero reasons to spare us.
reply
> recent work in animal communication

Worth noting that this is an invisibly small part of the sum total of our global efforts, especially versus the much more tangible effort we put into enslaving and slaughtering them, then mangling their carcasses for our own uses as we drive more and more of them to extinction.

We simply don't care about anything beyond ourselves and even there it breaks down on closer analysis when we see how many within our species don't truly value the collective whole beyond themselves.

It's just atoms all the way down.

reply
> enslaving and slaughtering them, then mangling their carcasses for our own uses as we drive more and more of them to extinction.

I'm frankly offended by this mischaracterization of human-animal relationships. So called "slaves" like horses and dogs have been dearly beloved companions for centuries and actively seek our companionship too.

The animals we raise for slaughter are often mistreated, yes, but many humans treat them with respect; billions on billions are voluntarily spent to improve their condition. Despite our own needs, many people pay higher prices for animal products that involve better treatment of animals. And they are in no risk of extinction! Much to the contrary, their domestic variants would not exist if humans didn't raise and protect them.

> We simply don't care about anything beyond ourselves

Have you seen modern westerners with their dogs??

reply
I think you’re splitting hairs. The OP’s analogy works well.

If we end up in a future where AIs have as much concern for our welfare as we have for the welfare of the average animal (not the minuscule percentage of domesticated dogs, but the overwhelming majority of factory-farmed or simply driven to extinction), then I doubt you would consider it a “mischaracterization” to say that the whole AI thing did not work out to our advantage.

Bringing up “modern Westerners with their dogs” as a counterexample is almost self-parody.

reply
Oh, don't get me wrong, I'm not rooting for a "human zoo" future. I very much like being the dominant species on earth.

It would be absurd to claim that all animals live some sort of charmed life due to humans.

But saying that animals (especially those most similar to us like intelligent mammals) are nothing more than "atoms" to humans is equally absurd.

reply
I don't think the analogy worked. It contained giant axes, and a giant grinder, and the OP shoehorned both into an unrelated discussion about math.
reply
> The animals we raise for slaughter are often mistreated

"Often mistreated". Dude, they are held in tiny cages injected with hormones and what not till we kill them so we can have a big mac. It's very hard to argue we do any of this for nutrition reasons, we do it because we like the taste of burgers and roast.

reply
The problem is not that AIs will somehow treat people badly, it's that they'll be controlled by humans who will treat other people badly using AI as a tool.
reply
Atoms are a lie.
reply
So it's lies all the way down?

I had suspected...

reply
> Things are currently moving fast. They cannot move fast forever.

This is a supposition that I fear will soon be proven false.

reply
It's a supposition that can only be proved true soon. To prove it false would take literally forever.
reply
This makes it sound like OpenAI and other closed source ai companies are an inevitability.

There is nothing here today that is unpredictable or impossible to control.

It is everyone's choice to let the greed continue, to let unelected sociopaths capture and feed society to the model.

It is not acceptable to put others at risk. It can stop and it can be done the right way instead.

That is, inform the industry that those causing these risks will be prosecuted regardless of their messiah complex.

The US government must not under any circumstances allow the ai industry to form a cartel.

We can make some effort to encourage open source models and thus stop the companies from causing hysteria by hiding the model, shrouding it it mysticism and prophesying the end times. China is doing a great service to everyone by making llms available to the public.

reply
Is it possible that we are now dealing with a human that has a complete understanding of whole mathematics while being unable have unique novel thoughts outside of convex hull of training data and their transitive expansions?
reply
I would say that disqualifies them from "understanding" anything. What they're doing is more like a broad search than pursuing a greater understanding
reply
Semantics
reply
You assume that LLMs are just summations of knowledge, implying that they do not create new knowledge. I doubt that this is the case. I mean, it comes down to the definition of knowledge, but as soon as you run LLMs, they can produce knowledge that has not existed before, and from my perspective, this is more like what we call thinking than it is just a reproduction of existing knowledge.
reply
Research seems to on balance point towards RLHF&RLVR merely increasing subjective sampling efficiency within the pretraining data.
reply
It doesn't seem clear whatsoever that this is true? Is there evidence that LLMs are very skilled at generalizing across domains of mathematics where the training distribution sees little overlap?

As far as I can tell, this is a victory for verifiable loops using LEAN, reinforcement learning, and oodles of compute. I haven't seen evidence yet that this is proof of broad generalization beyond the training distribution.

reply
I think such progress by agents is not a sign of broad generalization but of broad coverage. We have exposure to a subset of deeper scientific subfields and thus can only generate certain attacks to solve a particular problem. Since it is not clear which combination will lead to a solution beforehand it is nontrivial to look at a problem and fill our knowledge gaps. LLMs on the other hand have broad coverage and can generate hypothesis on a wide combination of subfields. With Lean an agentic loop can test these to sift the weak ones. In a way the problems solvable with this setup is also solvable by a human who happens to know the right subfields. These problems are likely to require an esoteric combination so nobody could solve them before. I really am not sure whether all generalization is like this or we can leap and create novelties beyond what an llm can generate. That I guess is the tough question that we need to answer to understand the boundaries of intelligence.
reply
Full quote is "Six years later we are beginning to understand the answer to this question. Machines have ingested the mathematics on the internet and are able to manipulate this data in a coherent way. The Erdős unit distance disproof came about because a machine happened to be an expert both in discrete geometry and class field theory; one rarely finds humans who are simultaneously experts in both"
reply
Similarly, there are probably many ideas that have not seen the light of the day because they require deep correlation between seemingly unrelated fields. It is not every day that we get a Isaac Newton or Leonardo da Vinci.
reply