leanuser83

you might like elinks as alternative to lynx, but with link hints.

and those shell aliases sound very similar to surfraw: https://en.wikipedia.org/wiki/Surfraw

That is exactly the point being made. That you can spot right away that something "doesn't make sense".

(Disclaimer: I'm addicted to Lean. My view is biased.)

Note that Lean is not so high on that list, but also note that serious theorem proving in Lean is less than 5 years old, whereas the other systems are (several) decades old. There are at least two entries on the list that have only been formalized in Lean, and not in any other system. We are catching up pretty quickly.

It's clear that this list has an important status. But in my opinion, building a library of undergrad maths, which is what what TFA is mainly about, is a lot more important. We are tracking our progress over at https://leanprover-community.github.io/undergrad.html

I am not aware of such an organized effort in other systems. Without such a fleshed-out undergrad library, we'll never get to systematic formalization of (post)grad mathematics.