What Is Lean?

lean is a computer proof checker. It listens to you carefully and picks up on anything you say that isn't precise. So we can type in mathematical proofs andn it will go through them, and at the end, if it believes them, then it will say, ye ok, sure, i get it. But what does it mean believe them? In lean's case, it means that it's taken the things you've told it, and it's translated those things right down to the barebones axioms of mathematics,. And checked that everything checks out.