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)

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)

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)