Questions on proof assistants

[Qian Hong]

Hi Joe,

I noticed that you didn't copy "Lean" from Freek Wiedijk's list, I
guess it's because there are only 29 theorems proved by Lean which
seems not very impressive.
However, I recommend you to try Kevin Buzzard's Natural Number Game
(implemented using Lean) and you might enjoy it:

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

(Disclaim: I'm not an expert of any of these proof assistants, I'm
just a beginner)