It doesn't. It's 32 millions lines of bullshit, and the only thing it brought is "it's not true in some extreme conditions lol". The effort needed to figure out why that is, what conditions lead to it, the new mathematics that would need to be developed to solve their problem is once again being hoisted on actual humans, who now need to waste their time sifting through their slop.
You don't have to read 32 million lines. You can just look at what got proved. The proof checker lets you trust those millions of lines you did not read.
No, you don't understand: that proof is useless. When you solve mathematical problems, you open up new ones in the process of doing so. You create new research. You create new theories, new notations, new thought.
This is just ticking a checkbox. And even worse and more time wasting even: you have ZERO proof that there's no latent Lean bug. Especially in a proof this large.
Not a Lean expert but some of the proof tactics used to prove are probably novel? Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?
>Not a Lean expert but some of the proof tactics used to prove are probably novel
Maybe. But they're in 32 millions lines of Lean. How do you find the needle in the haystack ?
>Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?
If OpenAI was truly serious about improving maths (and not jerking themselves off), they'd have also used Prove2Me (and contributed their results back), which would have done that. Each part of the proof combines into a larger graph, that everyone can reuse. Note that Anthropic isn't better there: yes, they used Prove2Me, but as far as I know they haven't contributed back to it, and just shat out 10 million lines and a good luck everyone.
Leaf dumps out a proof object that can be verified to be correct. Absent a bug in the verifier, you can trust it, probably more than you can trust a human-produced proof. This is why Lean was a thing even before AI.
