History of metamath_setmm
The changes to the source code of this entry in the repository, newest first, each with the differences it made to the entry's files. They are also listed on GitLab.
[entries] New entry: metamath_setmm 5ffaf08
diff --git a/entries/metamath_setmm/__init__.py b/entries/metamath_setmm/__init__.py
new file mode 100644
index 0000000..e7795c4
--- /dev/null
+++ b/entries/metamath_setmm/__init__.py
@@ -0,0 +1,260 @@
+#! /usr/bin/env python
+# -*- coding: utf-8 -*-
+#
+# Copyright (C) 2026 Tiago de Paula Peixoto <tiago@skewed.de>
+#
+# This program is free software: you can redistribute it and/or modify it under
+# the terms of the GNU Affero General Public License as published by the Free
+# Software Foundation, either version 3 of the License, or (at your option) any
+# later version.
+#
+# This program is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
+# FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for more
+# details.
+#
+# You should have received a copy of the GNU Affero General Public License along
+# with this program. If not, see <http://www.gnu.org/licenses/>.
+
+
+import re
+from calendar import timegm
+
+from .. import *
+
+title = "Metamath set.mm theorem dependencies (2015-2026)"
+description = r"""Dependencies between the theorems of set.mm, the main database of the Metamath project, a formalization of mathematics from first principles (classical first-order logic and ZFC set theory), with every step of every proof verified by machine. set.mm was started by Norman Megill in 1992, and has been developed collaboratively since then (on GitHub since 2015), with tens of thousands of theorems, from logic to real and complex analysis, algebra, topology and number theory.
+
+The nodes are the assertions of the database: the theorems (statements with a proof, `$p`), the axioms and the definitions (`$a` statements of the form `|- ...`), and the syntax constructors (`$a` statements of the other types, which define how formulas, classes and set variables are built, e.g. `wi` for the implication). A directed edge goes from a theorem to each assertion referenced in its proof (theorems, axioms, definitions, and syntax constructors used to build the formulas of the proof), with the number of times it is referenced. The hypotheses of the theorems (`$e` and `$f` statements) are not nodes, and are left out.
+
+The proofs are mostly stored in the compressed format of Metamath, where the steps reused within a proof are referenced once, so that the counts are of the references in the proof as stored (the number of times the statement is referenced in the compressed proof, which can be smaller than the number of times it is used in the fully expanded proof). Incomplete proofs (with unknown steps) keep the references they have.
+
+The database is updated continuously; the networks are of the database at the last commit of each year from 2015 to 2025 (`2015` ... `2025`, from the GitHub repository), and of 31 October 2026 (`2026`).
+
+The networks have the following properties:
+
+- `name`: the label of the assertion (e.g. `ax-mp`, `df-an`, `id`), whose page is `https://us.metamath.org/mpeuni/<name>.html`.
+- `kind`: `theorem`, `axiom` (`$a |-` statements other than definitions), `definition` (labels starting with `df-`) or `syntax`.
+- `statement`: the statement of the assertion, as Metamath symbols (e.g. `|- ( ph -> ph )`).
+- `part`, `chapter`, `section`: the headings of the part, chapter and section of the database in which the assertion appears (e.g. `CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY`, `Propositional calculus`); the users' mathboxes (personal sections of the contributors, with material not yet moved to the main body) are in the part `SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)`.
+- `contributor`: the contributor of the assertion, as given in its comment (usually the initials of a contributor of the list in the header of the database, e.g. `NM` for Norman Megill).
+- `contributed`: the date of the contribution as given in its comment, as Unix time (-1 if not given).
+- `discouraged`: whether new usage of the assertion is discouraged (as stated in its comment).
+- Edge `count`: the number of references to the assertion in the proof (as stored)."""
+tags = ['Informational', 'Relatedness', 'Weighted', 'Metadata']
+url = ['https://us.metamath.org/',
+ 'https://github.com/metamath/set.mm']
+citation = [('N. Megill, D. A. Wheeler, "Metamath: A Computer Language for Mathematical Proofs." Lulu Press, Morrisville, North Carolina (2019)',
+ 'https://us.metamath.org/downloads/metamath.pdf')]
+icon_hash = None
+upstream_license = ("CC0", "https://creativecommons.org/publicdomain/zero/1.0/")
+upstream_prefix = 'https://raw.githubusercontent.com/metamath/set.mm'
+# The last commit of the branch "develop" of each year, and the latest one
+_commits = [("2015", "b51d49674d85dba11542bb1f3f0a75ed9dcf0551"),
+ ("2016", "d3c116ab7db67993e022b3007b3f3ef508ec296d"),
+ ("2017", "8fc62600ecab6882174b6f35c1db5299287ce62f"),
+ ("2018", "2e21aa61bee33236705466b8577749eca49f5b82"),
+ ("2019", "f95b9b427eaedf4c18b794f357df2de71ba9d4f6"),
+ ("2020", "55fe226d84fca15cf4fbb6bcc0e3ee0e00fe640e"),
+ ("2021", "7455dd7bb5f5ca2b044371f720e67994a0da6750"),
+ ("2022", "7a4a1886b2a661013ba432e0b513aa1964a1608a"),
+ ("2023", "f81542d33adb25c56983a1325e060abe0e334156"),
+ ("2024", "f9d5a5229a02952910ce0a13e5e53906e671669b"),
+ ("2025", "cad4c6b1069b00ff7742b1bdc52314643ff3519e"),
+ ("2026", "3ec8669641b1ab6ddce7d51a0d7807ec83aa3403")]
+files = [(f"{sha}/set.mm", alt, None) for alt, sha in _commits]
+
+def fetch_upstream(force=False):
+ return fetch_upstream_files(__name__.split(".")[-1], upstream_prefix, files,
+ force)
+
+# Decoration lines of the headings of parts, chapters and sections
+_levels = {"####": 0, "#*#*": 1, "=-=-": 2}
+_contrib = re.compile(r"\((?:Contributed|Proof shortened|Revised) by ([^,()]+?),\s*(\d{1,2}-[A-Za-z]{3}-\d{4})\s*\.?\)")
+_contributed = re.compile(r"\(Contributed by ([^,()]+?),\s*(\d{1,2}-[A-Za-z]{3}-\d{4})\s*\.?\)")
+
+def heading(comment):
+ """The level and title of a heading comment, or None."""
+ lines = [l.strip() for l in comment.strip().splitlines()]
+ if len(lines) < 3:
+ return None
+ level = _levels.get(lines[0][:4])
+ if level is None or not lines[0].startswith(lines[0][:4] * 4):
+ return None
+ title = []
+ for l in lines[1:]:
+ if l.startswith(lines[0][:4] * 4):
+ return level, " ".join(title)
+ title.append(l)
+ return None
+
+_months = {m: i + 1 for i, m in enumerate(["jan", "feb", "mar", "apr", "may",
+ "jun", "jul", "aug", "sep", "oct",
+ "nov", "dec"])}
+
+def to_time(d):
+ "Dates such as 5-Aug-1993 as Unix time (-1 if invalid)."
+ try:
+ day, month, year = d.split("-")
+ return timegm((int(year), _months[month.lower()], int(day), 0, 0, 0))
+ except (ValueError, KeyError):
+ return -1
+
+def decode_compressed(letters):
+ """The numbers of a compressed proof (the "Z" marks are skipped)."""
+ nums = []
+ n = 0
+ for c in letters:
+ if "A" <= c <= "T":
+ nums.append(20 * n + ord(c) - ord("A") + 1)
+ n = 0
+ elif "U" <= c <= "Y":
+ n = 5 * n + ord(c) - ord("U") + 1
+ return nums
+
+def read_mm(f):
+ """Read a Metamath database, returning the list of its assertions, as
+ dicts with label, kind, statement, headings, contributor, date,
+ discouraged flag, and the counts of the labels referenced in the proof."""
+ text = f.read()
+ parts = re.split(r"(\$\(.*?\$\))", text, flags=re.S)
+ heads = ["", "", ""]
+ last_comment = ""
+ hyps = [[]] # active hypotheses per scope: (label, kind, symbols)
+ asserts = []
+ kinds = {} # label -> "a", "p", "e", "f"
+ # tokens, with the comments as tuples (comments can also appear
+ # inside statements, where they are skipped)
+ toks = []
+ for i, part in enumerate(parts):
+ if i % 2 == 1:
+ toks.append((part[2:-2],))
+ else:
+ toks.extend(part.split())
+ def strs(xs):
+ return [x for x in xs if isinstance(x, str)]
+ j = 0
+ while j < len(toks):
+ t = toks[j]
+ if isinstance(t, tuple):
+ body = t[0]
+ h = heading(body)
+ if h is not None:
+ level, title = h
+ heads[level] = title
+ for l in range(level + 1, 3):
+ heads[l] = ""
+ last_comment = body
+ j += 1
+ continue
+ if t == "${":
+ hyps.append([])
+ j += 1
+ continue
+ if t == "$}":
+ hyps.pop()
+ j += 1
+ continue
+ if t in ("$c", "$v", "$d"):
+ j = toks.index("$.", j) + 1
+ continue
+ label = t
+ kw = strs(toks[j + 1:j + 3])[0]
+ if kw in ("$e", "$f"):
+ k = toks.index("$.", j)
+ hyps[-1].append((label, kw, strs(toks[j + 2:k])))
+ kinds[label] = kw[1]
+ j = k + 1
+ continue
+ if kw == "$a":
+ k = toks.index("$.", j)
+ stmt = strs(toks[j + 2:k])
+ proof = None
+ j = k + 1
+ elif kw == "$p":
+ k = toks.index("$=", j)
+ stmt = strs(toks[j + 2:k])
+ l = toks.index("$.", k)
+ proof = strs(toks[k + 1:l])
+ j = l + 1
+ else:
+ raise ValueError(f"unexpected token {kw} after {label}")
+ kinds[label] = kw[1]
+ stmt = stmt[1:] if stmt and stmt[0] == kw else stmt
+ refs = {}
+ if proof:
+ if proof[0] == "(":
+ r = proof.index(")")
+ labels = proof[1:r]
+ # mandatory hypotheses: all active $e, and the $f of
+ # the variables of the statement and of the $e
+ active = [h for s in hyps for h in s]
+ vs = set(stmt[1:])
+ for h, hk, syms in active:
+ if hk == "$e":
+ vs.update(syms[1:])
+ m = sum(1 for h, hk, syms in active
+ if hk == "$e" or (hk == "$f" and syms[1] in vs))
+ for n in decode_compressed("".join(proof[r + 1:])):
+ if m < n <= m + len(labels):
+ x = labels[n - m - 1]
+ refs[x] = refs.get(x, 0) + 1
+ else:
+ for x in proof:
+ if x != "?":
+ refs[x] = refs.get(x, 0) + 1
+ if kw == "$p":
+ kind = "theorem"
+ elif stmt[0] != "|-":
+ kind = "syntax"
+ elif label.startswith("df-"):
+ kind = "definition"
+ else:
+ kind = "axiom"
+ last_comment = " ".join(last_comment.split())
+ c = _contributed.search(last_comment) or _contrib.search(last_comment)
+ asserts.append(dict(label=label, kind=kind,
+ statement=" ".join(stmt), heads=list(heads),
+ contributor=c.group(1).strip() if c else "",
+ date=to_time(c.group(2)) if c else -1,
+ discouraged="(New usage is discouraged.)" in last_comment,
+ refs=refs))
+ last_comment = ""
+ return asserts, kinds
+
+@cache_network()
+@coerce_props()
+@annotate()
+def parse(alts=None):
+ name = __name__.split(".")[-1]
+ for fname, alt, fmt in files:
+ if alts is not None and alt not in alts:
+ continue
+ with open_upstream_file(name, fname, "r") as f:
+ asserts, kinds = read_mm(f)
+ index = {a["label"]: i for i, a in enumerate(asserts)}
+ edges = []
+ for i, a in enumerate(asserts):
+ for x, c in a["refs"].items():
+ if x in index:
+ edges.append((i, index[x], c))
+ elif kinds.get(x) not in ("e", "f"):
+ raise ValueError(f"unknown label {x} in proof of {a['label']}")
+ g = Graph(directed=True)
+ g.add_vertex(len(asserts))
+ g.ep.count = g.new_ep("int")
+ g.add_edge_list(edges, eprops=[g.ep.count])
+ for k in ("name", "kind", "statement", "part", "chapter", "section",
+ "contributor"):
+ g.vp[k] = g.new_vp("string")
+ g.vp.contributed = g.new_vp("int64_t")
+ g.vp.discouraged = g.new_vp("bool")
+ for v, a in enumerate(asserts):
+ g.vp.name[v] = a["label"]
+ g.vp.kind[v] = a["kind"]
+ g.vp.statement[v] = a["statement"]
+ g.vp.part[v], g.vp.chapter[v], g.vp.section[v] = a["heads"]
+ g.vp.contributor[v] = a["contributor"]
+ g.vp.contributed[v] = a["date"]
+ g.vp.discouraged[v] = a["discouraged"]
+ yield alt, g