 Most databases (".mm" files) have an associated interface, called an "Explorer", which allows one to navigate the statements and proofs interactively on the website, in a user-friendly way.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.