THE LIVING ARCHIVE

From punched cards to autonomous collaborators: the ideas, people, languages and systems that taught machines to follow—and increasingly interpret—human intent.

PAST / PRESENT / NEXT

Collection

Tag: lean

Lean: From Interactive Theorem Proving to a Community Library of Formal Mathematics

Lean combined a small dependent-type-theory kernel with extensible proof automation and a practical functional programming language, then grew through Mathlib into a major community platform for machine-checked mathematics.

↗