Post #4105980

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.