Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.)

My comment on Kevin Buzzard’s intervention:

https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ

Link list of the discussion threads:

https://owlofminerva.net/kubota/update-to-the-foundations-of-mathematics/