Quanta Books @quantabooks.org · May 28 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)
3 likes 1 replies
?
Replies
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)