[runeblaze]

I mean sure we can do ZFC or ZF as the foundation, and I am sure with enough effort we can make metamath or some modern derivative great again. At some point though I like having years of type-directed program synthesis research helping me write proofs; I like type-checking research helping me check my proofs, and I like my proof assistants to work well for verified program extraction if I also happen to write code because the mathematics academic job market is quite shit for your average pure maths PhD, and if I were to do logic then it might be even shittier.

Admittedly the above (except program extraction I suppose) can all be achieved with ZFC + a layer of type theory on top, and again that's a reasonable thing to do, but I hope this makes a strong enough case for the type theoretical foundation.

[auggierose]

Type theory is definitely the dominant paradigm in current proof assistants, so yes, if you want an easy life, and your head doesn't hurt from unreflected type theory propaganda as witnessed here in this thread, do that.

But if you want an easy life, instead of trying to do what is right, why did you do math in the first place?

[runeblaze]

ZF(w or w/o C)/type theory/other foundations of maths are "equally" right? My argument is that even if we are trying to build PAs from scratch, type theory provides tangible benefits to the working mathematician because we can just borrow CS research in many stuffs like proof checking and synthesis.

Of course that is a benefit in the "meta" level, but it is not like ZFC is a better foundation than topoi/types/etc..

[auggierose]

There is nothing wrong with learning from CS research, but mathematicians are just better at thinking about mathematics than computer scientists are. Would you think in types if you didn't have to do it on a computer in a system designed by computer scientists? No way. Would you think in ZFC? Not really, either. We are now in a moment that might decide for the foreseeable future how we think about math, and we better get it right.

[runeblaze]

idgi tho. The average working mathematician seldomly thinks about proof theory or how proofs "work". Proof theory if must be put in a single box it is an logician's art, and at that point it is niche enough in both CS and maths that it becomes meaningless to say mathematicians know more about it. Logicians are better at thinking about proofs than either maths people or CS people.

I mean I don't know what you mean by right, but given how type theory/ZFC/categorical foundations there is no clear winner (unless you can make a good argument for set theory as our foundation, because again, the average mathematician seldomly thinks in ZFC), I'd say type theory is quite nice in its computational interpretations so let's go with that.

I also don't want to go there, but obviously research drains manpower and money. If we can get CS people to write PAs we really should do that. They're filthy rich in the grand scheme of research.

[auggierose]

How proofs work is really simple. The question is, how do you work inside a proof assistant, which kind of math is easy to express, and what is difficult? If you leave that to the CS people, math will become computer science. The ultimate logician was Gödel, and he clearly was a mathematician.

[runeblaze]

> How proofs work is really simple

idgi. If you do your 101 logic class often you learn natural deduction, and how do you formalize natural deduction in a computer system? (Hint: type theory is "natural" for this).

Also how proofs work is far from simple.

[kthielen]

What do you have to say about Curry-Howard?