julesh on Nostr: Science advances one funeral at a time, and a bunch of mathematicians who are ...

Science advances one funeral at a time, and a bunch of mathematicians who are currently young and betting their career on Lean are eventually going to be dinosaurs sitting on hiring committees and insisting to their grave that it is good actually that their favourite proof assistant falls over if you hit it with a corner case of dependent pattern matching on something defined with coinduction-corecursion or whatever