5 ms·
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.
by charcircuit 5d ago
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.
- well_ackshually 5d agoNo, 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.
- pyentropy 4d agoNot 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?
- well_ackshually 4d ago>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.
- pfdietz 4d agoLeaf 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.
- pfdietz 3d agos/Leaf/Lean/
- charcircuit 4d agoLLMs are good at finding the needle in the haystack. All efforts now should be in figuring out how to make LLMs get as good as possible at math.