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