Comment by groundzeros2015
19 hours ago
Type theory and lean is more interesting to people who like computers than to people who like math.
19 hours ago
Type theory and lean is more interesting to people who like computers than to people who like math.
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.
I think the most surprising thing I've learned taking formal math in college is just how much mathematicians are pragmatists (at least for my teacher with sample size n=1). They're much more interested in new ways to think about ideas, with a side effect of proofs for correctness. The proof is more about explaining why something works, not that it does.
I'm going to take a formal logic class in the fall, and my professor said something akin to "definitely take it if you're interested, just be aware that it probably won't come in use in most of the mathematics done today." The thing is the foundations are mostly laid, and people are interested in using said foundations for interesting things, not for constantly revisiting the foundations.
I think this is one reason most mathematicians don't see a need for formal proof assistants, since from their perspective it's one very small part of math, and not the interesting one.
This is not to say that proof assistants are a dead end—I find them fascinating and hope they continue to grow—but there's a reason that they haven't had a ton of traction.
I think that's a good way of putting it. I would addend that most people working in mathematics aren't generalists, their primary interest isn't in a broad picture. Rather, most are hyperfocused into a single domain with a strong backbone of reflexive intuition built up. By virtue of sheer human limitation, there's only so much someone can care about what's happening outside of their world while still making serious contributions within it. This doesn't even just extend all the way to shifting foundations, but number theorists can hardly be expected to keep up with the forefront of graph theory, for example.
For the pragmatists Logic as a field commits the immortal sin: it blasphemes the intuition that mathematicians spend years honing by obliterating it. Not just for a singular domain, but for all domains. Of course, that doesn't really explain the whole picture. Formalism built a holy walled city. Logicians, by nature of their work, leave the safety of the walled city to survey, exploit and die in the tangled jungle outside. Some don't even speak the holy language of the glorious walled city, they talk in absolutely gibberish modalities and hyperstructures. There is a political tension held against logic and logicians as a result.
Mathematicians use logic to talk about the mathematical world. But logic is not the world.
Not even the most dogmatic of the set theorists ever argued mathematics was possible without reason, however. For mathematics, logic is the world, as the copula makes no distinction between substance and existence. In the same sense that the earth is not matter itself, but it is a material thing.
Putting that aside, to make things more clear: computer science is mathematics. Computer scientists are mathematicians. That was a categorization decided long before you and I ever lived. In the sense that you mean, you're only referring to a very small fraction of what "mathematics" refers to In the true sense of the word. It is just as irreconcilably disjointed as Logic is, not unified and fundamentally non-unifiable.
I too think it would be better if "mathematics" was reserved for the gated suburb of ZFC. But that's not the world we live in, courtesy of the same people who pushed ZFC as a foundation to begin with.
1 reply →
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.
Formalised proofs and Lean in particular are still too cumbersome for the ``working'' mathematician to use it day-to-day for research-level math. But clearly there is some interest on where it may take us in future.
> one of the most important living
Maybe. But more clearly one of the most popular online.
He's a Field's Medalist so that's automatically one of the most important living. He is good at explaining things; I leaned on his Analysis textbooks when I was taking analysis and functional analysis to great effect; in a research class I was trying to calculate Fourier transforms of algebraic sets and found various almost throw away comments on his blog that were extremely enlightening (alas only to the extent I could follow them). He's a legit great mind of modern mathematics - and also able to communicate well; a historical rarity indeed.
The topic being discussed here has been addressed specifically in his mastodon posts - the pre-LLM math process was understood to be "state a proof, validate a proof" - but the real aim was the not explicit "digest the proof so we can extend to other results" - with LLM/lean making the first two a lot easier and possible to do without accomplishing the digestion into the mathematical community; so we need to add "digesting proofs (from where ever)" into the job description. Thread starts here: https://mathstodon.xyz/@tao/116477351524980995
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 link is exactly what I’m saying. I only hear cs people talk about it.
For mathematicians a proof is a means to an end, or a medium of expression - they care about what they say and why.
The correspondence isn’t about C programs corresponding to proofs in math papers. It’s a very a specific claim about kinds of formal systems which don’t resemble how math or programming is done.
Mathematicians care about interesting ideas, not whether their theorems are true :-)
5 replies →