On the Lean proof assistant, Part 1
A long time ago I became interested in proof assistants. I tried Isabelle and Coq for sure and I might have tried Mizar. Here, ‘try’ could mean tried to install and failed. Some of them worked, but I quickly gave up using them. In all of them the documentation was bad and I couldn’t figure […]