Comment by yieldcrv

Because they want to release everything on github so everyone can peer review it themselves

This is far more efficient and they’re telling the academic industry to grow up

Sister comments are saying that academics dont like the Lean programming language and see a lack of human language described proof. Doesn’t sound like something I should care about but I’m watching for a better human language description of the problem as this discussion evolves