Comment by ezwoodland
8 hours ago
You can only do so in another framework that might itself have bugs.
Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean".
The kernel does have bugs sometimes.
I consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.