Computers can directly prove some theorems today, and in other cases there are various interactive provers that let humans and computers work together to find f

Computers can directly prove some theorems today, and in other cases there are various interactive provers that let humans and computers work together to find formal proofs. In some systems using computers can give much better confidence that the proof is correct, because computers are very good at carefully checking every step; nitpicking is their forte and they don't get tired. Freek Wiedijk maintains a list of 100 challenges for math formalization and the status of various systems here: http://www.cs.ru.nl/~freek/100/ http://www.cs.ru.nl/~freek/100/ - Formalizing 100 Theorems Lean hasn't accomplished as many as some others, but it's certainly a contender!