Comment by jojomodding
2 days ago
Math is not about the definitions. It is about the connections between these definitions. And the techniques used to establish broader classes of connections between similar objects.
The way we formalize a connection is with a proof. And if the proof is "nice and modular" it sorta explains by itself how it can be used for similar problems.
And such proofs definitely belong into MathLib. There is often value in actually reading the Lean proof script (especially with the IDE support like jump to definition). It is not only there for the machine.
Proofs are not nice and modular though unless they can be extracted into a macro/tactic (or theorem), which I said belongs. They are literally not reusable. The perspective I'm coming from is that we should extract what is valuable as elevated theorems, leaving only the not-so-valuable technical details as the proofs. The connections between objects are theorems.
Lemma, Theorem, Proof, Repeat.