Comment by Syzygies

https://github.com/Syzygies/Compare

I spent far too long comparing dozens of languages, only some of which are part of the above project, before switching from Haskell to Lean for a new phase of my math research. Lean wins for me without considering or using dependent types (for now). It is simply a better programming language than any I have seen.

This is a critical advantage for those interested in proof. One codes tactics using the same language as for proof.

https://github.com/Syzygies/Compare/blob/main/source/lean/Na...

I do have a future interest in proof, giving Lean an edge for me. I prefer my symbolic reasoning in visual form. I anticipate a future where we draw and view AI drawings, and see any printing press derived notation as antiquated as cuneiform. The above image is a possible language for representing the first Lean proof in "The Natural Number Game". About one in ten mathematicians that I show this to can grasp it much faster than the Lean notation. The other nine imagine a visual programming language to be something like a PowerPoint slide or a children's graphics language, and don't see the point.