As Kevin Buzzard recently said:
> In a 2020 piece in the Notices of the AMS, I asked the following question: “If one human had an understanding of all of modern pure mathematics simultaneously, how much further would they immediately be able to see?” Six years later we are beginning to understand the answer to this question.
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)
>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..
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)
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.
I'm trying to be optimistic about the animal thing too tbh :)
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.
> 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.
> 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. And they are in no risk of extinction! Much to the contrary, their domestic variants would not exist without us eating them.
> We simply don't care about anything beyond ourselves
Have you seen modern westerners with their dogs??
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.
If you think AI-generated Lean proofs are unreadable, imagine Opus 5 generating informal proofs.
I think OP is saying Lean does indeed help.
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.