One verification project, Metamath, includes human-written, computer‐verified derivations of more than 12,000 theorems starting from ZFC set theory, first order logic and propositional logic.
Un proxecto de verificación, Metamath, inclúe deducións de máis de 10.000 teoremas a partir dos axiomas de ZFC e usando lóxica de primeira orde.