The fact remains though that Lean 3 worked well enough to do Scholze level mathematics. I never quite know what to make of people saying "if the designers had done it in some other way, it would have been better". Of course if someone comes along doing it another way, and then they go on to also achieve Scholze level mathematics, then I will be all ears.