Lean 4
A rare system where theorem proving and serious programming share one language, one toolchain, and one culture.
The Iron Formalist Medal
For proving that a theorem prover can also be a serious programming language.
Why It Belongs
Lean 4 is a dependently typed functional programming language that also serves as an interactive theorem prover. It is the engine behind Mathlib and one of the few systems where formal mathematics and practical programming genuinely inhabit the same environment.
It belongs in the Hall because it closes a gap that many systems merely gesture at. Lean does not force you to choose between writing proofs and writing programs; the same language handles both, and the tooling makes the proof workflow feel like real software work rather than ceremonial punishment.
What To Preserve
Preserve the language, the tooling, and the proof-programming unity that gives the system its identity.
What matters is not just that Lean can verify theorems. It is that it proves formal methods can live in a serious developer toolchain without feeling exiled from ordinary programming practice.
Related Inductees
Adjacent artifacts, tools, and internet relics
The Order of Inverse Sorcery
For creating a program that feels impossible, useful, and slightly illegal.
RIES — Robert Munafo's Inverse Equation Solver
The original RIES program by Robert P. Munafo. Given a real number, finds simple algebraic equations that have that number as a solution.
The Order of Mathematical Public Service
For making it possible to look at a strange sequence of integers and ask the internet what universe it belongs to.
OEIS — The On-Line Encyclopedia of Integer Sequences
A monumental reference work for integer sequences: part encyclopedia, part mathematical commons, part search engine for pattern recognition.
The Grand Archive Laurels
For lifetime achievement in public weirdness, mathematical density, and internet maximalism.
mrob.com — Robert Munafo's Website
A sprawling personal site covering mathematics, large numbers, fractals, cellular automata, and more. The kind of website that used to be common and should still be.