Post

The programming language and math proof assistant Lean is the latest tool in a millennia-long search to discover and verify the truth. A thread: (1/7)

In the fourth and third century BCE, Aristotle and Euclid laid the groundwork for rigorously verifying mathematics by representing it as a formalized, rational, symbolic language that could be objectively evaluated. (2/7)

Later, Bertrand Russell and Alfred North Whitehead’s Principia Mathematica (1910-1913) proposed a new formal system—type theory—for expressing, verifying, and maybe even discovering new mathematics. If the foundation was solid, maybe the resultant structure would be too. (4/7)

In 1931, Kurt Gödel shook the world with his incompleteness theorems, which argued that there were limits to knowledge: no formal system—a set of rules from which all else was supposed to follow—could ever be complete. Even then, Gödel was optimistic about formalized math. (5/7)

Today, Lean continues this legacy of truth-seeking, giving mathematicians a powerful, interactive tool with which to fulfill Gödel’s dreams of “prov[ing] any theorem using nothing but a few mechanical rules.” (6/7)