metamathGraph is the dependency graph of theorems .... where its nodes are “generalized substitution” taking in some set of theorems, and generating a new one [each node is a proof of one named theorem from others] [the “raw material” may include “definitions”, which have the same form as axioms]
Base of everything is named operator-like constructs
Dependency graph is coarse-grained to the level of just talking about named theorems, eliding away unnamed lemmas
MM database defines 35241 things that were named....
Of which XXX are definitions, XXX are axioms .... and XXX are derived theorems
Definitions define syntax forms but don’t have truth value