The Proof in the Code

Let's take a look at the Lean programming language!

Lean theorem prover is a tool where code is types and programs are proofs.

We learned in grade school that 2 + 2 = 4 easy. But how do we know? Together we will use Lean to make a proof as code
🧩

#PLnerd