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 seventeenth century, Gottfried Leibniz dreamed of a universal symbolic language, his characteristica universalis, that he believed would be capable of expressing—and verifying—any rational thought. Formalizing, rather than fighting, would resolve disagreements. (3/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)