Everyone credited

Who did the work

238 people and 8 libraries are named across the 629 credited formalizations on his page. The table on the front of this site shows each of them as a dot; this is the page that says whose dot it is.

Compressing a formalization to a mark is what makes the shape of the data visible, and it is also the one place this redesign is worse than what it replaces: he wrote a name where there is now a glyph. Every filled cell in the matrix still carries its credit — hover one, or read it with a screen reader, and you get "Metamath: formalized by Norman Megill" — and this page is the other half of that repair.

How this list was made, and what is wrong with it

His credits are free text, written by hand over twenty-five years, and they do not parse cleanly into a list of people. Of the 629 that carry a credit, 64 name more than one person with an &, 79 contain a further comma that might be another person or might be a note about which library the proof lives in, and several name a project rather than a person. This list is therefore a reading of his credits, not a fact derived from them.

The raw credit is what the site treats as authoritative: it is what the matrix renders, what a screen reader announces, and it is shown against every formalization below so you can see what was read and disagree with it. Where splitting was ambiguous, the six credits with parentheses were written out by hand rather than guessed at, and three people who appear under two spellings — Artur Korniłowicz, Yury G. Kudryashov and Johannes Hölzl — were merged. Those were found by reading all 246 names, because no automatic comparison finds them: ł is a letter rather than an accent, and neither is oe for ö.

Four pairs here share a surname and are not the same person — two Andersons, two Trybulecs, two Rodriguezes and two Liangs — so a tidier list would be a less accurate one. One credit, on #68, names nobody at all: it reads "not in contribs, many versions", which says where the proof is and how many of it there are, and never says who wrote it.

Among the names is Claude Code, credited with six HOL Light formalizations including #21, Green's Theorem, one of the six he marks as a serious challenge. On a list kept by hand since 1999, on a page that has never had a framework, that seemed worth pointing at rather than letting it pass as one more row.

Read from a copy of his page as he last modified it on 2026-04-09. Every theorem number links to its row on the list, and the credit each was read out of is on the link itself.