Hacker News new | ask | show | jobs
by jon-wood 7 days ago
I'm sure its technically possible, you might need to provide a bit more context if you expect anyone to change course here and port it to a programming language approximately no one has heard of rather than Rust though. What makes you think that would be a good idea?
1 comments
koito17 7 days ago
> approximately no one has heard of

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.

link
HeavyStorm 7 days ago
Oh, PhDs, you're right, that's not approximately no one... It's probably approximately one.

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.

link
jcelerier 7 days ago
Apparently roughly ~150k math PhDs live on earth right now, assuming they all know Lean that's between 0.001% and 0.002% of earth population so quite closer to no one than one
link