Not only are the proofs long and unintelligent, but they don't cite previous work.

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.

▲

Animats a day ago | parent [-]

"Polish this paper. Check all proofs with Lean. Try to find shorter proofs of lemmas where possible. Write for a undergraduate math student. Add brief explanatory material as needed. Cite previous work where relevant. Check all citations. Convert to LaTeX."

▲

cloudbonsai a day ago | parent | next [-]

I’m wondering why frontier labs haven’t done that.

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.

▲

famouswaffles 5 hours ago | parent | next [-]

For A, a common misconception is that models write out lean proofs from the start. They write/develop the Natural Language proofs, and then translate (sometimes not even the same model) to lean afterwards.

▲

Animats 15 hours ago | parent | prev | next [-]

The four-color theorem appears to be case C. That was the first really long computer-assisted proof. No one has since found a concise way to do that proof, and it's been half a century now.

	▲	cloudbonsai 11 hours ago \| parent [-]
		I'm not sure how Terence Tao's "digestion" concept holds up if the upcoming AI math results are all like that. It would be almost like humans are chewing bones under the table, while LLMs are feasting.

▲

mmooss a day ago | parent | prev [-]

D. They seek disruption as way to market dominance and worldly power. It's not unfortunate, in their minds, but the means to their ends.

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!'

	▲	2snakes a day ago \| parent [-]
		Doctorow talks about this dynamic in his book about reverse centaurism. It is a “growth story” for investors.

▲

emil-lp 14 hours ago | parent | prev [-]

Funny.

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.).