Introduction

How much math can a computer do? And could computers ever get really good at it? If that sounds far fetched, well just remember what happened in chess not so long ago. A small but growing community of mathematicians has been busy writing code in a programming language called lean. They're building a library of math knowledge to help human mathematicians check their proofs. Will they ever move from being mere proof assistants to genuine proof creators? And if so, will mathematicians like me and my guest ever be out of a job?