Tag Archives: lean

Proof assistants and the future of math

posted by on Tuesday December 29, 2020 with No comments! and filed under philosophy, technology | Tags: ,

Are proof assistants the next breakthrough in mathematics? This is a question I have been thinking about since I tried the Lean proof assistant. I have tried proof assistants before, but Lean feels like it’s on another level. For one, I actually wrote a natural deduction proof in it. I can easily imagine it being […]

On the Lean proof assistant, Part 1

posted by on Monday December 14, 2020 with No comments! and filed under computer-science | Tags:

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 […]