alt Hacker NewsI'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?
> 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.