I consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.