#metamath — Public Fediverse posts

So, just double-checking how #Lean4 and #Mathlib work:

* Lean takes 3GiB of RAM and a minute to open Mathlib
* Lean requires about 10min to build itself in CI, only verifying required theorems
* Verifying all of Mathlib is measured in hours
* Lean's kernel is untrustworthy due to junk theorems

And yet I'm a clown for using #Metamath? At some point we ought to reconsider the type-theory fetish.