Formal proof

You can build a mathematical library like the Lean Math Lib.

So in Kevin's book, Proof in the Code, he gives a precise definition of a kernel, which is a component in an interactive theorem prover like Lean.

An interactive theorem prover has two basic components.

A logical foundation, which determines how ideas are expressed and interact with each other.

And so, you know, what I like about logic is that it's somewhere between mathematics, computer science and philosophy.

So here at Carnegie Mellon, my primary appointment is in the philosophy department.

Proof assistance started just kind of as a hobby, just messing around with them because I thought they were interesting around the year 2000.

So