Questions on proof assistants

Qian Hong fracting at gmail.com
Wed May 13 00:57:42 EDT 2020


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)


More information about the FOM mailing list