In fact, they completely disregard all standards of mathematical dissemination. They just post a bunch of 100+ page papers online and call it the day.
A real mathematician polishes and polishes for months until it is understandable by the community. Then they communicate the results to a journal where there are editors and peer reviewers who come with detailed feedback which is then implemented. And just then it is ready to publish.
A few possibilities I can think of are:
A. The capability is just not there. OpenAI and Anthropic can produce a brute-force Lean proof, but their models aren’t capable enough to digest the proof as human mathematicians do.
B. They haven’t seriously tried it yet. They prioritized grabbing the land first, and have not spent much effort to polish things up.
C. It’s fundamentally impossible. These theorems are provable only in a very ugly manner. This is the reason why human mathematicians haven’t been able to crack them before AI in the first place.
As a programmer, what I’m seeing is (C). Many recent cyber hacks are products of AI trying & combining every possible tricks, and I don’t think there is any elegant short path that human engineers can replicate.
Disruption has been a SV buzzword for a long time now. It's not a byproduct but a strategy for your new technology product. SV has long perfected disruption and the people behind the AI products are masters at it.
How can so many who have seen it (and used it) for so long be so taken in by this well-worn tactic. Over and over, they choose what is most disruptive. They could have dealt with the mathematical output in many ways, including working with mathematicians to polish and publish; you see what OpenAI chose.
Similarly was the recent events where AI software 'broke containment' and hacked others. Obviously they could have controlled it if they valued it; they got the result they wanted. Notice how Anthropic (or were they first and OpenAI followed?) urgently publicized that their product, too, 'broke containment'. 'We're disruptive too!'
The problem is that this is not something that LLMs (currently) can do.
Lean has nothing to do with understanding and intuition.
Brevity of proofs are also not the target.
The target isn't undergrads, either, but all of this is pointless because LLMs aren't up to this task (p.t.).
Let's take an example: Maxwell's 1865 paper states electromagnetism as 20 equations in 20 unknowns, written out in components. His 1873 Treatise recasts parts of it in quaternions, which was even more esoteric. The four vector equations everyone learns are Heaviside's, from 1884-85, five years after Maxwell died. The clean form came from other people working on the ugly original. Had Maxwell waited until he had something elegant, it would have been a net negative to society. Yes there was cleanup but I would argue that's a part of learning and understanding.
I think part of this mentality is a perfectionists view that does not always align with our "messy" reality.
I wish mathematicians would just focus on this. This really is the problem, at the end of the day.
Having models get better at writing elegant proofs and explaining their results will not solve this problem - it will only make it worse, if anything.
We are all sympathetic to this. I, personally, am much less sympathetic to the absurd notion that it is "bad" that this new technology can solve important open mathematical problems at all, that we should stop trying to solve them, that things like the Mathathon are dangerous and needs to be shut down, that ugly proofs are the real problem here, so much so that you wish the open question weren't resolved at all, and so on. So silly.
But being pissed off that people are going to be out of work is something I agree 100% on. Hopefully, much like the internet, there's a way to make the whole thing a net benefit for society.
I don't see it. What I see is more wealth and power concentration and with the worst group of people possible.
But really bad from a social perspective - as people lose their jobs they also lose their tiny piece of power in the society that was the labor someone else needed. Now that power has concentrated to the frontier model owners, and everyone in the future will depend on them.
And on a personal level, sacrifices people have made to become good at their craft have been made worthless, as any rich PoS can now prompt their way to "good" art and call their end result as good as something made with skill that needed years of training. That I really hate.
Which is only possible because:
a) The models have been trained on work of millions of people,
b) They've done it for free, In other words, they've stolen entire people's lives. Millions of lives. They literally suck people dry and tell them to go look for another job.