Proof in the Code

The inside story of Lean, a computer program that answers the age-old question: How do you know if something is true?