[vilhelm_s]

Yeah. I guess the abstract type approach saves some memory, but it's a constant factor thing, not an asymptotic improvement. The comment that Lean wastes "tens of megabytes" seems telling: it seems like something that would be a critical advantage in the 1980s and 1990s, when Paulson first fought these battles, but maybe less important today...

[nrds]

To be fair, lean wastes and leaks memory like a sieve, but this is almost all in the frontend. It has nothing to do with the kernel or the theorem proving approach chosen.