3 ms·
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 ("th
by ezwoodland 1mo 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.
- DoctorOetker 1mo agoI consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.