This project develops a framework for classifying mathematical statements—such as theorems, lemmas, corollaries, and axioms—based on their structural roles and perceived significance within formal mathematics. We use the Metamath database set.mm, which encodes mathematics as a network of formal proofs, and represent it as a directed dependency graph, where an edge from A to B indicates that A uses B in its proof. Using the Wolfram Language, we analyze this graph to extract and quantify features such as proof length, centrality scores (e.g., betweenness, PageRank), expression similarity, and reachability. We define categories of interest—including easy, difficult, important, useful, elegant, boring, corollary, and interesting theorems—based on measurable graph-theoretic properties. This classification offers a structural lens on the architecture of formalized mathematics, enabling us to explore the mathematical network beyond symbolic content and toward conceptual organization. The framework is scalable and can support future tools in automated reasoning, mathematical search, and curriculum design.
Introduction
Introduction
Formalized mathematics has quietly grown into one of the richest and most intricate data structures we possess. With projects like Metamath and Lean, vast swaths of mathematical knowledge are now encoded in databases where every logical step is explicitly tracked. Yet despite this precision, we rarely explore these databases not just as repositories of truth, but as networks of meaning. What if we could treat mathematics itself as a terrain to be mapped? What if we could say not just that a theorem is true, but that it is deep, elegant, useful, or trivial—not based on intuition, but on its location in a graph? Inspired by Stephen Wolfram’s vision of mathematical statements as nodes in an ever-expanding proof network, this project aims to classify theorems using ideas from graph theory and computational analysis. Throughout the project, we ask questions such as: Which theorems are foundational? Which are short, beautiful, and surprising? And which are just… boring? By analyzing the Metamath set.mm database as a directed graph of dependencies, we use various type of centralities, proof length, expression similarity, and other metrics to uncover the structural roles that theorems play. Ultimately, this is an experiment in mathematical cartography—an attempt not just to prove theorems, but to understand their place in the universe of mathematics.
Introduction to Metamath and Set.mm
Introduction to Metamath and Set.mm
Metamath is a tiny, flexible, and ultra-minimalist language and system for representing formal mathematics. It provides a rigorous framework for encoding mathematical logic, where every proof step is explicitly justified down to the most primitive axioms and rules. Rather than relying on high-level tactics or automation, Metamath emphasizes complete transparency: each derivation is human-verifiable and machine-checkable. At the heart of Metamath is the Metamath Proof Explorer, a massive database of formalized theorems written in this system. The largest and most famous of these databases is set.mm, which develops a substantial portion of standard mathematics—including logic, set theory, number theory, real and complex analysis—entirely from first principles. Because of its formal rigor and explicit structure, set.mm offers a unique opportunity to study mathematics as a computational object—not just for verifying proofs, but for analyzing the roles different theorems play within the entire corpus.
Understanding the Dependency Graph
Understanding the Dependency Graph
At the heart of this project lies the dependency graph constructed from the Metamath set.mm database. This graph encodes the logical structure of formal mathematics by representing how theorems, axioms, and definitions are used to prove one another. In this graph, nodes represent mathematical statements (e.g., axioms, definitions, lemmas, theorems) and directed edges represent proof dependencies (that is, there is a directed edge from node A to node B if statement B is used in the proof of statement A ). This means the graph flows backward through logical derivation: from complex theorems to foundational results. Its structure is a Directed Acyclic Graph (DAG) — there are no cycles, since proofs cannot be circular. We use Nikolay Murzin’s MetamathImport tool from the Wolfram Function Repository, which provides a high-level interface for parsing Metamath source files directly within the Wolfram Language. The function takes a Metamath source file (e.g., “set.mm”) and returns a MetamathObject containing the full structure of statements, types, dependencies, and more. From this object, we extract the dependency graph. This graph becomes the basis for the structural analysis in our project — including centrality computations, clustering, and theorem classification based on various graph-theoretic and token-based metrics. The dependency graph turns Metamath into a mathematical network, opening it up to insights from graph theory and data science.
Quantifying Theorem Characterization
Quantifying Theorem Characterization
To understand the roles and significance of individual theorems within the Metamath database, we treat the dependency graph as a mathematical network. In this network, each node is a theorem, and edges represent proof dependencies. The structure of this graph encodes not just which theorems are provable, but how knowledge is built up — which theorems support others, which are frequently utilized, and which sit at the core of mathematical development. Our approach is to quantify the position and influence of theorems using various network centrality measures, which are well-established tools from graph theory and network science. These measures help us assign numeric scores to theorems based on their structural roles in the graph. By applying these measures, we aim to numerically characterize theorems.
Characterization of Theorems
Characterization of Theorems
We begin by importing the database. The original dependency graph g includes theorems, axioms, and syntactic definitions. This full dependency graph represents each mathematical statement as a node, with directed edges indicating proof dependencies. A directed edge from B to A means that statement B is used in the proof of A. The graph includes foundational elements such as axioms and syntax rules. To isolate the pure network of theorems, we removed nodes with no outgoing edges, as these typically represent statements that do not require proofs—primarily axioms or syntactic definitions. After this filtering step, we are left with exactly 45,617 theorems from the original database. Interestingly, although only around 6% of the nodes are axioms or syntactic definitions, this removal eliminates nearly half of all edges in the graph. This highlights their foundational role—being directly used in the proofs of a vast number of theorems. The significant reduction in edges also offers a key insight: on average, theorem proofs rely almost equally on foundational principles (axioms/syntax) and on previously proven theorems.
Lemma
Lemma
A lemma is a relatively short theorem that plays a supporting role—typically appearing at an intermediate stage in the proof of other theorems . In our dependency graph, an edge A → B means “B is used in the proof of A”. This means that the more incoming edges a node has, the more frequently it appears in other proofs. Therefore, the in-degree of a node is a good measure of its “lemmaness”. So theorems with high in-degree are strong candidates for lemmas, as they are widely utilized in proofs across the database. To identify candidate lemmas, we examine the distribution of vertex in-degrees in the theorem-only graph. Theorems with significantly higher in-degrees than the median can be considered lemmas, as they are frequently reused in the proofs of other theorems.
Iconize[mm=ResourceFunction["MetamathImport"]["SetMM"]];g=mm["DependencyGraph"];Iconize[theoremVertices=Select[VertexList[g],VertexOutDegree[g,#]>0&]];gTheorem=Subgraph[g,theoremVertices];Iconize[InDegrees=AssociationThread[VertexList[gTheorem],VertexInDegree[gTheorem,#]&/@VertexList[gTheorem]]];ListLogLogPlot[Sort[Values[InDegrees],Greater],PlotStyle->Red,PlotLabel->"In-Degree Rank Plot (Lemma Candidates on Left)"]toplemmas[num_]:=TakeLargestBy[InDegrees,Identity,num];Subgraph[gTheorem,Keys[toplemmas[100]]]
Corollary
Corollary
We approximate corollaries as theorems with short proofs that depend on exactly one important theorem (identified via high betweenness centrality). This captures the idea of results that naturally follow from fundamental theorems with minimal additional effort, highlighting how new insights often build directly on key mathematical foundations. To clearly define “easy theorems,” we select those whose proof lengths fall within the lowest 10th percentile of the overall distribution. This percentile-based threshold meaningfully identifies the shortest proofs, reflecting results that require minimal reasoning steps relative to the full body of theorems. For each easy theorem t, we check whether its dependency set intersects with exactly one important theorem. This isolates corollaries as those easy theorems whose proofs rely on a single foundational result, emphasizing simplicity and direct logical flow within the dependency network.
betweennessScoregth=BetweennessCentrality[gTheorem];assocbetwgth=AssociationThread[VertexList[gTheorem]->betweennessScoregth];easyThms=Keys@Select[proofLengths,#<=Quantile[Values[thmprooflengthassoc],0.1]&];(*shortest10%*)importantThms=Keys@Select[assocbetwgth,#>=Quantile[betweennessScoregth,0.9]&];(*top10%*)corollaries=Select[easyThms,With[{deps=VertexOutComponent[gTheorem,#]},Length[Intersection[deps,importantThms]]==1]&];
{mpd,mpi,id,idd,pm2.43i,notnotri,alimi,2alimi,ala1,ax7v1,ax11dgen,ax12dgen,bj-1,bj-nnclav,bj-nnclavi,wl-embant,iidn3,idiVD}
Easy Theorem
Easy Theorem
An easy theorem is simply one that has a short proof. This means it requires fewer logical steps, fewer dependencies, or simpler arguments to reach the conclusion. More formally, the “easiness” of a theorem can be understood by measuring the size or length of its proof in the dependency graph. Since we removed the axioms and syntax definitions, this can cause to underestimate the proof length. So we will work with original graph g.
theorems=Select[mm["Statements"],Head[#]==="Theorem"&];getproofsteps[thm_]:=Module[{prfstps},prfstps=Take[DeleteCases[thm[[4]],"("],FirstPosition[DeleteCases[thm[[4]],"("],")"][[1]]-1]];proofLengths=Length@getproofsteps[#]&/@theorems;thmnames=First/@theoremsIconize[thmprooflengthassoc=AssociationThread[Keys@thmnames,Values@proofLengths]];
Here is the one of the most easy theorem and its description:This inference says “if 𝜑 is true then 𝜑 is true”.
Difficult Theorem
Difficult Theorem
A difficult theorem is one that requires a long proof, meaning it depends on many intermediate results and reasoning steps. Such theorems typically encapsulate deep or complex mathematical ideas that cannot be resolved quickly. Proof length reflects the complexity of logical derivation.
Elegant Theorem
Elegant Theorem
In addition to proof length and importance, another fascinating classification is elegant theorems—those whose statements are both concise and distinctive within the body of mathematics . Elegant theorems have brief, compact statements. These are results expressed with few symbols or tokens, capturing powerful ideas succinctly. Beyond being short, an elegant theorem should be somewhat unique — its statement should stand apart from others rather than being a slight variation of common patterns.
We already have theorems tokenized into sets of symbols or tokens . To capture uniqueness, we use the Jaccard similarity between these token sets. The Jaccard similarity measures the overlap between two sets as the size of their intersection divided by the size of their union. A low Jaccard similarity with other theorems indicates a unique or uncommon statement. Combining these two properties, We first select theorems with short statements (e.g., in the shortest 10% of expression lengths), then, for these short theorems, we compute pairwise Jaccard similarity scores to identify those that are least similar to others, reflecting their uniqueness. The method runtime is out of hand for whole database. So we will make it only theorems that has certain number of short expression. To better capture true elegance in theorems, we restricted our analysis to those with expressions containing at least four´ tokens. This decision helps exclude trivially short theorems—such as those consisting of a single token—that, while syntactically minimal, are often straightforward consequences of basic axioms and lack deeper structural insight. By focusing on theorems with slightly more complexity, we aim to highlight results that are not only concise but also encapsulate meaningful mathematical ideas in a compact form.
Interesting Theorem
Interesting Theorem
We define interesting theorems as those that are both non-trivially derived and highly connected within the proof dependency graph. Non-trivially derived means the theorem’s proof is complex or deep, not easily deduced from a small set of earlier results — this is reflected by a high out-degree (many dependencies). Well-connected means the theorem plays a significant role in the broader proof ecosystem — this is captured by a high in-degree (used in many other proofs) and high centrality. Such theorems lie at the intersection of complexity and influence: they require substantial foundational work to prove, and in turn, they serve as essential components in proving many others.
Boring Theorem
Boring Theorem
To identify theorems that offer little novel structure or conceptual contribution, we define boring theorems as those that are highly similar to many others in the database. Since we tokenized the theorem expressions and compute average Jaccard similarity of it, then theorems with the lowest uniqueness scores can be classified as boring, reflecting their structural redundancy or role as routine variations of more general principles. This metric helps reveal repetitive patterns within the formal system and distinguishes mechanically necessary statements from conceptually rich ones.
Useful Theorem
Useful Theorem
Useful theorems are those that play a foundational role in the development of many others. In the dependency graph, such theorems tend to have high in-degree, meaning they are utilized in a large number of subsequent proofs. To quantify this influence more robustly, we use PageRank centrality, which captures not just how many times a theorem is used, but also how important the theorems that use it are. This recursive definition mirrors the idea of foundational knowledge rippling through the structure. Originally designed to rank web pages, PageRank models a random walker on the graph and assigns higher scores to nodes that are more likely to be visited — analogous to how often a theorem is indirectly invoked in mathematical reasoning. Thus, PageRank is a meaningful tool to identify central and critical theorems that form the structural backbone of formal mathematical development.
Surprising Theorem
Surprising Theorem
To identify surprising theorems, we combined two complementary graph-theoretic measures: vertex eccentricity and degree centrality. Vertex eccentricity captures how far a theorem is from the rest of the network by measuring the longest shortest path to any other node. A high eccentricity suggests that a theorem lies in a peripheral or sparsely connected region of the dependency graph. Meanwhile, a low degree (few direct dependencies or uses) indicates limited local interaction. Surprising theorems are those that exhibit high eccentricity and low degree, yet still play meaningful structural roles. These are theorems that, despite their apparent isolation, act as hidden bridges between distant parts of the network or introduce unexpectedly useful insights. By surfacing such results, we uncover nodes that defy their sparse surroundings and highlight the less obvious, yet impactful, contributions within the formal system.
Important Theorem
Important Theorem
Betweenness centrality is a graph theory measure that tells us how often a node (here, a theorem) lies on the shortest paths between other nodes in the graph. In our case, betweenness centrality identifies theorems that frequently appear as critical dependencies in shortest proof chains. These theorems act as essential bridges connecting many different results by serving as fundamental building blocks in proofs. Thus, high betweenness theorems unlock broad areas of mathematics by being commonly used across multiple proofs. So we can pick important theorems with help of high betweenness centrality. In the full graph, high betweenness nodes may include axioms, definitions, or syntax constructs that serve as fundamental building blocks used across many proofs. These foundational nodes often act as critical “gateways” or hubs connecting large parts of the graph. Their presence can inflate or shift the betweenness centrality rankings compared to a theorem-only graph. In the theorem-only graph, the betweenness centrality highlights which theorems themselves are essential connectors in the network, independent of underlying axioms or definitions. This isolates the proof-level structure and may reveal theorems that function as “key lemmas” or “bridge results” within the mathematical landscape.
Conclusion
Conclusion
This project explored the Metamath set . mm database through the lens of graph theory to understand how formal theorems function structurally and conceptually . By analyzing dependency relationships as a directed graph and applying centrality, similarity, and eccentricity measures, we classified theorems into categories such as useful, boring, elegant, surprising, and powerful . These categories helped reveal deeper patterns in theorem usage, redundancy, and connectivity within formalized mathematics . The framework not only offers a novel perspective on the internal dynamics of formal systems but also provides tools that could assist in proof assistant automation or educational insight . Future work may extend this analysis to larger subgraphs, apply geometric or topological interpretations, or integrate these structural insights into interactive theorem - proving environments .
References
References
CITE THIS NOTEBOOK
CITE THIS NOTEBOOK
Classifying mathematical statements via Uuing Metamath dependency graph
by Botan Cevik
Wolfram Community, STAFF PICKS, July 10, 2025
https://community.wolfram.com/groups/-/m/t/3497782
by Botan Cevik
Wolfram Community, STAFF PICKS, July 10, 2025
https://community.wolfram.com/groups/-/m/t/3497782