About

The project, and this redesign of it

Formalizing 100 Theorems is a record of which theorems from a 1999 list of the hundred greatest have been proved in a machine-checked proof assistant. Freek Wiedijk keeps it, at Radboud University Nijmegen, and it is the closest thing formalized mathematics has to a scoreboard: 661 formalizations, 13 systems, hundreds of named contributors, one page.

What it tracks, and what it leaves out

The list of theorems is not his. It is "The Hundred Greatest Theorems", presented by Paul and Jack Abad at a mathematics conference in July 1999 and ranked on "the place the theorem holds in the literature, the quality of the proof, and the unexpectedness of the result". What he added was the tracking, and he is blunt about the list's limits: "This list (which I did not make!) has some obvious omissions."

He also does not try to record every formalization ever done. In his words the page "just shows formalizations in systems that have formalized a significant number of theorems, or that have formalized a theorem that none of the others have done" — so the 13 systems here are the ones that earned a column, and each of their communities keeps its own list of the hundred as well. Where a theorem's entry names several systems, they appear "in the order of the list of systems, and not in chronological order".

Of the hundred, 99 have been formalized at least once. The list of theorems people have written to him about as missing from the 1999 list runs to another forty-one, which he keeps at the foot of the page — alphabetically, and marked for whether they have been formalized anyway.

How something gets onto the list

There is no form, no tracker and no submission process: this is one person maintaining a page by hand. Formalizations and corrections reach it the way the missing-theorems list did — someone tells him. If you have proved one of the hundred in a proof assistant, or spotted something wrong here or on his page, email is the route, and the credit line under the theorem is where your name goes.

How to reach him

Freek Wiedijk is an assistant professor at Radboud University Nijmegen, working in the project of Henk Barendregt and Herman Geuvers. His own homepage is where all of this is published, and it notes that his name is pronounced like "Phrake Weedike".

Mention free ultrafilters in the subject line. That is his instruction, not a joke at his expense: he asks senders to "mention free ultrafilters in the subject line of your message" so that his spam filter lets it through.

These are his published work details, read from his homepage on 2026-08-12. He lists a home address and a mobile number there too; they are deliberately not repeated here.

About this redesign

This site is not his and is not endorsed by him. It is a student exercise: an unsolicited redesign, built for a course crit, of a page whose content is entirely his work. The data, the credits and the outbound links are his, taken from a copy of his page as he last modified it on 2026-04-09 and fetched on 2026-08-05. He is still updating it; this is a snapshot, and his page is the canonical source.

What the redesign changes is the presentation, and the argument for it is short: the data is a hundred theorems by 13 systems, and his page shows it as one column 538 pixels wide with no mobile viewport at all, so on a phone the text runs off the edge. This version puts the grid on the page, replaces meaning-by-italics with marks that a screen reader can read out, and fixes a contrast failure his visited links have had for years. It keeps what makes his page good: no framework, no tracking, and nothing fetched at runtime.

The links that differ from his

His outbound links are carried across as they are — including the ones that go to a plain http:// host, because that is where those pages actually are. two of them are not, and these are they. Each was opened in a browser rather than assumed, on the date given; his URL is still what the underlying data records.

• For the 1999 list itself, personal.stevens.edu → pirate.shu.edu: his link returns a 404: Nathan Kahl, who hosts the list, has moved institutions and it moved with him to Seton Hall. Verified as the same document — "The Hundred Greatest Theorems", Paul and Jack Abad, July 1999, and its first entry is the irrationality of root 2, as his is. http-only, deliberately not upgraded: https times out on that host. Checked 2026-08-12.
• For Isabelle's statements, on all 92 of its rows, www.cse.unsw.edu.au → pruvisto.github.io: his link returns 403 in a browser, not just to a crawler, so it is dead for a reader too. The list has a maintained successor kept by Manuel Eberl, and it numbers its anchors exactly as the old one did — #1 is the irrationality of root 2, #33 Fermat's Last Theorem, #99 Buffon's needle — so every per-theorem deep link still lands on the right theorem. Checked 2026-08-12.

Repairing a link rather than dropping it is a judgement call, and it is the one place this redesign changes his content rather than its presentation. The alternative was to hand a reader 92 links in the table that go nowhere, and one more for the list itself.