Visualize the dependency of mathematical theorems and proofs. A blend of the Bourbaki tradition, formal proof system, reverse mathematics, and readable prose.