- lean proofs are hard, and a lot of the time there is so much mathematical machinery that folks are working on that you would need to not only prove your result, but also all of the machinery that your subfield it is built on. it would be infeasible for many authors to do all of this work (this might be a major part of multiple careers, and when there are 5 folks in your entire subfield, the payoff is not really worth it)
- human proofs are readable, and can illustrate concepts better than lean proofs. human proofs give insights into how to think about a type of problem, and this is often the most valuable part of a proof/result.
- lean proofs are often very difficult to read; while they give you a "verified" check mark, they do not necessarily improve the bounds of human understanding if that makes sense.
Wondering: if the process for the upper part of the sandwich is the complement of the process for the lower part, why was it so much more difficult? What would go wrong if you took one of the earlier lower-sandwich processes, and complemented it in a similar way? I have to assume it's something, but what?
Is there a central repository of lean proofs shared by mathematicians like an npm repository of JavaScript packages?
Does it all depend on a stupid is-odd package in the end?
- lean proofs are hard, and a lot of the time there is so much mathematical machinery that folks are working on that you would need to not only prove your result, but also all of the machinery that your subfield it is built on. it would be infeasible for many authors to do all of this work (this might be a major part of multiple careers, and when there are 5 folks in your entire subfield, the payoff is not really worth it)
- human proofs are readable, and can illustrate concepts better than lean proofs. human proofs give insights into how to think about a type of problem, and this is often the most valuable part of a proof/result.
- lean proofs are often very difficult to read; while they give you a "verified" check mark, they do not necessarily improve the bounds of human understanding if that makes sense.