For reference, Lean is a computer program that checks mathematical proofs for correctness by translating them into formal logic.

In case you want to watch Terence Tao, an actual mathematical genius, at work.