Post

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)