Skip to main content

All Questions

Filter by
Sorted by
Tagged with
1 vote
0 answers
53 views

Does there exist a database of formalized definitions and theorems based on NBG set heory?

Is there a library of formalized mathematical definitions and theorems similar to Lean's mathlib, but based on Von Neumann–Bernays–Gödel set theory and first order logic, rather than type theory? I am ...
5 votes
0 answers
165 views

Formal and informal proofs: Is there any "bilingual corpus"?

There are extensive libraries of formalized mathematics like those of Lean, Coq or Isabelle/HOL. What I am interested in is documents of formalized mathematics that closely follow certain informal ...