 Most databases use a Hilbert system of formal deduction though this is not a requirement.The Metamath Proof Explorer (recorded in "set.mm") is the main and by far the largest database, with over 23,000 proofs in its main part as of July 2019.It is based on classical first-order logic and ZFC set theory (with the addition of Tarski-Grothendieck set theory when needed, for example in category theory).