Just cause it isn't used for webshit doesn't mean "approximately no one" has heard of it.
Lean is pretty much the most popular language mathematicians use today for computer-assisted proofs. More mature audiences may know about Rocq, Isabelle, etc., but Lean was already popular enough for a few people I know to have written their PhD theses on it about a decade ago.
I think GP is joking about a port to Lean because that would at least produce a formally verifiable output.
I like Lean (and more generally dependent types) but ffs Lean has a very, very small userbase for a project like this. GGP would have to really justifyv the benefits for such a switch.