alt Hacker NewsType theory and lean is more interesting to people who like computers than to people who like math.
Replies
I would’ve expected that people who like computers will converge around something like Idris. It’s marketed as a development tool, not a tool for formalizing mathematics even though it could be used as a proof assistant.
Terence Tao, one of the most important living mathematicians, specifically embraces Lean and has been helping the community embrace it.
What you've done here is an overgeneralization. "People who like math" and "people who like computers" are massive demographics with considerable overlap.
citation needed, Tao certainly is on record using Lean and that carries some weight.
also, https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... i.e. there's no reason it should be as you say.
The set theorists decided that mathematics is the overarching superdomain over all study of structure. You don't get to pick and choose. Either mathematics is a suburb of logic and these two things are separate, or they're not and ZFC dogmatics need to accept they don't have a monopoly on math.
I of course fully support reinstating logicism, but the same dogmatics love putting up a fight over that as well.