One post tagged with "formalization"

Freek Wiedijk's list of one hundred mathematical theorems has long served as a compact way to understand the reach of a theorem-proving system. It is broad enough to touch much of ordinary mathematics, but concrete enough that progress can be measured theorem by theorem. A prover that makes progress on the list has to do more than manipulate syntax. It needs a library, a mathematical vocabulary, proof search, replayable proofs, and enough ergonomic surface area for people to keep building.