Remix.run Logo
groundzeros2015 3 hours ago

Type theory and lean is more interesting to people who like computers than to people who like math.

ux266478 3 hours ago | parent | next [-]

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.

smj-edison 2 hours ago | parent | next [-]

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.

ux266478 23 minutes ago | parent [-]

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.

groundzeros2015 3 hours ago | parent | prev [-]

Mathematicians use logic to talk about the mathematical world. But logic is not the world.

ux266478 2 hours ago | parent [-]

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.

groundzeros2015 2 hours ago | parent [-]

> For mathematics, logic is the world, as the copula makes no distinction between substance and existence.

No. There are truths about the subject not captured in any single formal system. Which is why objects are studied form many perspectives.

> Computer scientists are mathematicians.

Some are and some aren’t.

soulofmischief 3 hours ago | parent | prev | next [-]

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.

groundzeros2015 2 hours ago | parent [-]

> one of the most important living

Maybe. But more clearly one of the most popular online.

baq 3 hours ago | parent | prev | next [-]

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.

groundzeros2015 3 hours ago | parent [-]

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.

gowld 2 hours ago | parent [-]

Mathematicians care about interesting ideas, not whether their theorems are true :-)

groundzeros2015 2 hours ago | parent [-]

They care about if it’s true. But the role of the formal proof is a kind of spell checker or static analysis after they have the idea.

j16sdiz 2 hours ago | parent [-]

> They care about if it’s true.

Not always.

If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.

BigTTYGothGF 5 minutes ago | parent [-]

> If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.

I trust you have some examples of this?

3 hours ago | parent | prev [-]
[deleted]