(continued from discussion in random stuff thread)

Mathematicians rarely prove things in a logic where proof-checking is decidable. They prove things in some form of intuitionisitic logic, usually with higher-order functions. SOME (possibly most, but I don't know) of those proofs COULD be translated into a proof in a logical system with computable proof-checking available, but (almost) nobody does it. And few people care enough to even have a sentence that says "this proof can *clearly* be made using this amount of logical power, so, we are cool".

Can you elaborate what you mean with the first sentence? Can you give a specific undecidable logic where you think mathematicians work in?

I think most mathematician have faith that both their theorems and their proofs can be encoded in - for example - ZFC in classical first order logic, which is AFAIK the most accepted foundation of mathematics under mathematicians. Checking a formal proof in this logic is super decidable (I

*think *linear in the length of the proof). Higher-order logics (intuitionistic or not) can also be decidable, such as the

intentional Martin-Löf type theory. True,

*extensional* type theory is undecidable, but I'm claiming that mathematicians rarely work specifically in extensional type theory (if only because they don't specify in which logic they work, and hence their informal proof can be formalized in many logics, some of which are decidable).

Or are you talking about another problem: translating mathematical proofs on paper accepted by other mathematicians to rigorous formal proofs in some (decidable) logic? I agree that such a translation is infeasibly hard, but I think this problem is too vague to say that it is undecidable. I think that if a proof contains enough details, it should be possible to translate it into a formal proof. This is what happens with proof assistants all the time.

There is some value in the generalization, of course, which is mostly connecting things that were seemingly disconnected. My point is that there is also a loss in value because the proof done directly on the subject at hand is much more illustrating on the phenomena the person reading the theorem is interested in. So, my point is not that category theory is useless (although I think category theory is a drug at this point, kind of like string theory for mathematicians), but that it is over-praised as the ultimate tool and even the only thing that is worthy (or legit...).

So, to come back to my original post, more general is not always better. I agree with you that it is sometimes better and I would add that it is usually incomparable.

Caveat + example: My very first paper on my PhD topic is a simple combinatorial proof of a fact that was already known, but required to combine more general results from three different papers. Doing that lead to the ability to produce results for similar scenarios which an author of one of those papers was unable to get despite working in the question for some time.

I agree that a simple elementary proofs has a lot of merits. However, I do prefer a simple general proofs over complicated elementary proofs. And it is pretty common that a proof becomes simpler in a general setting. For example in category theory, there's often just one thing you can do in a proof, which makes proofs not that hard to find. More specifically about category theory: I'm neither saying that it is "the ultimate tool" or that it's the only worthy thing. However, I do think it's a very useful and very important tool. You might be interested in

this (short) answer on stackexchange which gives examples where category theory has been useful for other fields of mathematics.

And yes, in the end, a general theory is not strictly better, so a more general and a less general theory are incomparable, but I think the more general theory is better in 9 out of 10 aspects.