It's not really a matter of what formal system is most powerful. It's a matter of what formal system can represent ordinary math in the simplest and clearest fashion. I think this what proponents of category theory argue. Basically, category theory lets one take many standard mathematical theorems and generalize them widely - ie, lot of standard math theories can be seen as theories about categories and when you see them that way, the generality of a category means the theorem applies broadly.

I know category theory is popular in CS-land but over in math land it falls squarely in the "general nonsense" bucket for most working mathematicians.

E.g. most mathematicians learn the definitions of categories and the Yoneda Lemma perhaps as a chapter in some other text -- say a text on more modern algebraic geometry -- and that's about it.

The thing to understand is that mathematicians have jobs to do like everyone else -- they are not philosophers sitting in contemplation, but eager beavers trying to answer specific questions and solve open problems. So they are interested in picking up the tools that will help them solve unsolved problems more than picking up the tools that will help repackage the research of others. And the main feature of category theory is its ability to repackage the discoveries of others, rather than necessarily driving new research.

That's not to say that occasionally category theory can't be useful, but just not that many people are going to be working in those research fields where they find anything beyond the chapter's worth of Yoneda lemma plus some of the diagram formalism to be useful, and everyone's time and attention span is limited to what will help them make discoveries in their field.

Rarely is the answer to the question of how to solve some problem in differential geometry, pdes, number theory, symplectic geometry, combinatorics etc, -- "more category theory". The same is true for formal logic. Most people learn the incompleteness theorems and maybe even some things on computability, but they do not use formal logic to advance their research agenda, even though in theory proofs can be encoded in formal systems and so in some sense, these formal systems are a unifying framework to view mathematical proofs.

On the other hand, there have been some spectacular breakthroughs with physics/string theory, so a lot of people were trying to brush up on that. But here, too, progress is quite difficult, and most people aren't going to go out of their way to invest too much time in it beyond a summer school or so.

I share your view of what working mathematicians think like on this subject. I summarize it thus: how many interesting theorems are there in Category Theory? And the answer you get from proponents varies, but it seems to be like 1-3 with some being kind of a stretch. I would love to learn of a body of theorems like those of analysis or topology or algebra, but by comparison there seems to be very little "there" there. I would be happy to be proven incorrect on this!

Yeah, there's a lot of confusion for people using concepts like morphisms as a notation in their work versus category theory as a research program in and of itself. I don't think there is any research program there. But a lot of the more abstract topics like Motives use this language of morphisms and so people consider that to be category theory as well. I've even heard of people calling all the diagram chasing techniques like spectral sequences category theory, but I have to keep pressing the notation versus ideas distinction and give that a firm "no". If we start organizing mathematical subjects by their notational or bookkeeping systems, then we will not end up with useful categories (so to speak:)).

I am personally interested in this, as a cryptography PhD student, because the state of “provable security” is an absolute dumpster fire. In my opinion this is one particular application where machine-checkable proofs need to be established as a baseline standard.

Mathematics is not a jobs program—we should be building on previous work in the most efficient and effective way we can, and getting everyone to use standard techniques that easily translate to mechanizable proofs is the only way that is going to happen.

There are very few areas where mechanizable proofs have had success in math. I think some of the classification of finite groups was done with computer assistance, and some of the cases of the four color problem as well. But basically these are hand-crafted programs. Think of someone telling you that software engineers will be replaced by software writing computers -- that was the (failed) promise of UML. This is one of those situations where the software is generally not smarter than the person writing the code, and mathematical research, at any point in time, is driven by about 2-300 of the smartest people alive in the world at any time, with another few thousand adding finishing touches and elaborations on their work, and perhaps 10,000 adding small marginal adjustments to it. The idea that mathematicians' jobs are going to be automated by software is orders of magnitude less likely than the idea that software engineers will be automated by software. Lots of grand plans, but not much in the way of productive, transferable progress.

My comment was not to imply that software will replace people “doing math”, but that the math which is “done” will be encoded in a standard format that can be reused (and verified) more readily.

Really, this is about software—if you want to do anything with a computer, it must be formalized. Some of this formalization takes place before a line of code is written, usually in the form of mathematical statements. I’d argue that this part of the process ought to be standardized just like library code is standardized, or we will be carrying a very heavy load of collective technical debt as software is asked to do more and more complex and high-assurance tasks.

I don't quite understand -- we know that, for example, correct program analysis is theoretically impossible. There is no tool to verify a general software program. Why should there be a tool to verify a general theorem? Verification is at least as complicated as writing the program you are verifying.

> Why should there be a tool to verify a general theorem?

We want to verify proofs, not theorems. And that's far from "theoretically impossible."

Sorry, of course I meant to say "proof". A proof is just a more general case of a program. A program has logical operations, variables, control flow, etc. You can include all of these elements into a proof, and often do. Every program can be made into a proof, but not every proof can be made into a program. If you can verify the correctness of an arbitrary proof, you can verify the correctness of an arbitrary program. And even in practice many of the reasoning errors that happen in proofs also happen in programs -- forgetting to consider unforseen cases, not being correct about the possible ranges of variables, not anticipating all the external inputs into the program, making incorrect assertions about the state of variables, etc.

> Every program can be made into a proof

I'm not sure what you mean by this, but in my usage it's exactly the other way around. A proof can easily be interpreted as a program (as per the BHK and similar interpretations) but to interpret a program as a proof of something, you at least need to also formally prove that it halts. Edit: your edit clarified things a bit. The control flow in formal (and informal!) proofs is restricted compared to the control flow in programs: in order to do recursion or loops, you must have a formal argument that the recursion / loop terminates.

So normally when we say "proof", we assume the proof is correct. But in this discussion we are talking about possibly incorrect proofs, with the goal of verifying the correctness of the proof. So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true. Things like loops do appear in proofs as quantifiers. So for example a proof may perform a sequence of steps in which some set is depleted, and conclude that "as we must deplete all the elements the set, the claim holds", but determining whether all elements are actually depleted by the algorithm spelled out in the proof may be hard. These types of claims appear in actual proofs, and the types of errors that are found in proofs often boil down to some case being not considered which would cause the set not to be depleted.

Update: I'm unable to reply due to hn recursion limits, but as to your strictly smaller argument, that is not enough with infinite sets, which are common in proofs. Consider a proof about all surfaces, which you think you divided into a countable number of cases, but in reality there are some other types of surfaces you haven't considered. In math you are making assertions, in some sense, about the world, albeit the mathematical world, and you are claiming to have explored all the relevant parts of it for the sets of interest, but you may have not explored some parts you didn't know existed. The idea that you can formally verify such a sequence of claims is .. mind boggling. There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.

This is all a bit vague, so I may be misinterpreting here. But in the given example, the proof must also prove that at each step the set is getting strictly smaller, so the computer still only has to check that the proof is correct. That is, it doesn't have to check for itself whether the set is getting smaller, it just asks you to prove that the set is getting smaller in a way that it understands.

Anything more fancy than that is left up to proof automation, which is free to give up and say "nope, that leap's too big for me."

> So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true.

I'm not sure that's a good way of looking at it. I think the right image is to think of a proof as a program, and checking the proof as typechecking the program. The program has the additional restriction that whenever it does loops or recursion, it has to prove that something is getting strictly smaller with each iteration.

Wrt your update,

> The idea that you can formally verify such a sequence of claims is .. mind boggling.

Eh, if you're convinced that something's correct, it's not too mind-boggling that you can also explain it to a computer, given that it accepts all the same basic assumptions that you do.

> There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.

Yep: it looks like Lean is making good progress on their goal of formalizing the "undergraduate curriculum," but that's only the tiniest sliver of math. Math is hard, and doing it formally is even harder, so all I'm saying is that contrary to your earlier statements, it's definitely possible.

> Verification is at least as complicated as writing the program you are verifying.

I guess, writing a proof is basically like writing a program. Then checking a proof ought to be like *running* a program, not proving an arbitrary property of it. If your proof/program evaluates to "false", it's a wrong proof. So this is all a question of having an appropriate semantic model of computation/proof-checking, on which you can check your proof.

You could then ask: "why is it that I can always run a proof? What if running it does not terminate?" To which I'd have to admit that I am really, seriously not an expert on this, but I vaguely recall that interactive theorem proving systems like Coq have a non-Turing-complete type systems. Maybe it's for a relevant reason?

Nobody seriously thinks they can automate mathematicians, arguably the most creative people on the planet, out of a job.

Edit: also, I think you're wrong in saying that mathematical research "is driven by about 2-300 of the smartest people alive," but that's a rant for another time.

Perhaps look into Metamath Zero / mm0 which.. well I'll just quote from the project [1]:

> Metamath Zero is a language for writing specifications and proofs. Its emphasis is on balancing simplicity of verification and human readability of the specification. That is, it should be easy to see what exactly is the meaning of a proven theorem, but at the same time the language is as pared down as possible to minimize the number of complications in potential verifiers.

> The goal of this project is to build a formally verified (in MM0) verifier for MM0, down to the hardware, to build a strong trust base on which to build verifiers.

[1]: https://github.com/digama0/mm0

> I am personally interested in this, as a cryptography PhD student, because the state of “provable security” is an absolute dumpster fire. In my opinion this is one particular application where machine-checkable proofs need to be established as a baseline standard.

As a non-cryptographer and generally a layman, I wonder how useful machine-checked proofs about crypto are in security. What do they tell you?

The underlying reason for my skepticism is best illustrated with Spectre: it made architecture people sweat bullets, but also rendered previous applications of formal methods less useful. What good is a formal proof that a crypto algorithm is constant-time, if it assumed a model of computation that is a research toy? You can only verify properties that you can formulate within a given semantic model. I suppose, for hardware those are way less understood than for programming languages.

(Which is not to say that formal verification is hopeless of useless as it is. Just really curious what kind of proofs a crypto person would benefit from machine-checking, and how.)

Wasn't Spectre a hardware-level vulnerability and not at all related to cryptography? I remember it being something along the lines of, the way the CPU cache worked could be exploited and allow an attacker to read the data it contained. Correct me if I'm wrong.

You are absolutely right! I brought up Spectre not meaning to say it's an issue for cryptography (although maybe it is? it's above my paygrade :) ), but to illustrate one issue with formal proofs in security that I am trying to resolve for myself.

Spectre is a hardware-level vulnerability, which is based on how the code executed under misspeculation (the processor makes a branch prediction, executes stuff and then figures out the prediction was wrong) leaves detectable traces in cache. Technically, that is not specified, because caches and speculative execution are not a part of architecture. This renders security proofs at higher level of abstraction not necessarily correct or simply non-applicable (think properties like whether a program executes in constant time or if it is sandboxed), if they rely on the ISA being all that there is to know about hardware. Now, Spectre specifically might be "solved" as a problem, but the proof-minded people would be concerned with how to prove that. How to prove that things like this are not a security issue: https://asplos-conference.org/abstracts/asplos21-paper148-ex...

And to do that, it turns out they need to extend the models under the hood of their proofs with speculation semantics. A non-trivial task by itself, I bet it would trigger non-trivial conceptual changes to mechanized proofs too, so this all might be a labor-intensive game of catch. Alternatively, one could raise a question about what fully formal security proofs we want. Formal proofs make explicit assumptions about the underlying model of computation. Some of those assumptions might not hold because we (incorrectly) thought we could abstract some complexities of hardware away. Is that alright for the kind of security properties we want to have proven? It might be for some, but not others.

So with this in mind, I am curious how crypto experts think about properties they want to prove for their work. What value would the crypto community seek to extract from formal proofs? Are leaky abstractions an issue for them? It's all very interesting.

one thing where proofs are invaluable is the security of distributed systems where you need to exhaustively consider many uncoordinated actors.

The thing with “solving open problems” is whether one is solving particular instances of an abstract problem or a general case of a practical problem.

The latter is what software engineers call “design patterns.

Regarding what proponents of category theory argue as the purpose of category theory, [nlab] has some extremist takes, [chan] has a video series that shows us how a math student is typically sold on learning category theory, and [bauer] is a video which explores using a corner of category theory to formalize some basic computability results in a very different way to the usual formalism centered on Turing machines.

[nlab/0]: https://ncatlab.org/nlab/show/nPOV

[nlab/1]: https://ncatlab.org/nlab/show/applications+of+%28higher%29+c...

[chan]: https://www.youtube.com/playlist?list=PLgAugiET8rrLkzTFuwmiV...

[bauer]: https://vimeo.com/510188470

This kind of foundational (ZFC,CT,HTT) stuff is pretty niche in mathematics. Set theory, though touted as the foundation of math, isn't really used to its full extremes (HOD, etc) by anyone but set theorists. Its more like... A common datatype? And while CT could also be a foundation, as far as im aware its only practical uses as a tool are found in commutative algebra.

I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.

> I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.

I agree -- most fields of math are happy to establish their own axioms, and leave the reducibility of those axioms to some "foundations" as an exercise -- an important one, but not one that necessarily furthers the field itself.

However, Voevodsky's stated aim for his Univalent Foundations project was not to formalize everything under a grand theory of everything. He got the bejeebus scared out of him when one of his results was very, very subtly wrong, in a way that was difficult for mathematicians to verify for years, even given a reasonable inkling of a counterexample. So he sought to improve the state of the art in proof verification.

You might argue, it's better to produce a verification tool for one field of mathematics than all of them at once. But you'll have a hard time finding any significantly complex theorem that doesn't draw insight from multiple places. (Arguably, that's why they're significantly complex in the first place). And all fields of mathematics have some basic elements in common. So, I'd argue, you're unlikely to do a good job for any but the most narrow domains of mathematics without seeking some level of generality.

Any "foundation of mathematics" can be used for this purpose, and plenty of theorem provers have been built on each (Twelf, PVS, Agda). The draw of category theory is that it seems to capture at a fundamental level many of the basic conceptual elements we see across mathematics. (Homomorphisms are so universal it's not even funny.) It seems reasonable to pick something that starts us closer to where we want to be; the difficulties we encounter are more likely to be fundamental problems and not issues of encoding.

Couldn’t agree more. I am a current (mid career) PhD student in cryptography and WOW is it a mess. Provable security arguments are generally written in the implicit propositional logic + set theory of working mathematicians, but it is woefully inadequate for the job. Some very powerful composable frameworks have been developed, but they are really straining against the clunkiness of the formal system in which they have been constructed. The best new ideas I’ve seen for formalizing cryptographic settings all belong in category theory or topology, but have been formalized in set theory because that seems to be the only tool that the average cryptographer intuitively knows how to use.

Im not opposed to the use of proof assistant software for difficult theorems. And if one foundation or another is more applicable to that software, then thats fine.

Its more the narrative of the grand unification of mathematics thats spun around 'foundational theories' that irks me. In reality its just various emulation schemes.

Rephrasing other mathematicians work and claiming fundamental status, while not producing many novel theorems... just strikes me as very distasteful.

Only if one allows their ego to get in the way of the search for abstract truth does this become “distasteful”.

There’s no claim of fundamental status here, merely a desire to standardize aspects of what is very much an artisanal process.

In addition to CT's application to commutative algebra, it's pretty nice for reasoning about programs and logic.

Programs: http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen..., https://blog.sumtypeofway.com/posts/introduction-to-recursio..., the Functor/Applicative/Monad hierarchy in Haskell et al

Logic: https://publish.uwo.ca/~jbell/catlogprime.pdf

CT as a bridge between programs and logic: https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

All formal systems have their limitations as far as what is provable.

Example:, for any statement A unprovable in a particular formal system F , there are, trivially, other formal systems in which A is provable (take A as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel’s first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today’s “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.

This is well known. Type theories also do not assume the law of excluded middle. What's your point and it's relevance to the comment?

The issue is not one of “power”—one can make almost any formal system sufficiently “powerful” by adding a few axioms that get you over the rough spots in your proofs.

The problem is that the modern world increasingly relies on mathematics, in nearly all aspects of life, to make consequential decisions about how to interpret data and act on it. The challenge is not one of power, but of fidelity—using a mathematical structure that is a suitable abstraction for the real world situation. Use the wrong abstraction, and you end up with paradoxes like the incompleteness theorems.

I believe a goal of univalent foundations is to make the abstract structure that one is working with absolutely explicit, evidenced by the (almost) total absence of axioms from the system. If you want to work in ZFC, you can add those axioms yourself.

An interesting thing happened when category theory was used to model sets. It turned out set membership was problematic. When wearing your category theory glasses "parameterized elements" (subobject classifier) were the natural thing. Think tangent planes to a sphere instead of points on a sphere.

Isn't that a similar idea to the Hilbert program, which failed due to godel's incompleteness theorem?

Hilbert's program was about whether every statement could be proved ab nihilo either true or false. The question remains: given a proof, can we verify it? Arguably, any proof conceived by a human mind should be verifiable in principle. So the Incompleteness Theorem doesn't really apply, either formally or morally.

A more interesting argument could be made on the basis of Rice's Theorem: for a Turing-complete language, the only non-trivial properties provable about a program are fundamentally syntactic. (Type systems can be seen as a way of elaborating your syntax to capture finer-grained details of your semantics). Here we have a richer and nearer-to-hand collection of programs whose properties are inaccessible -- take, for instance, whether the 3n+1 algorithm halts on all inputs. Again, though, if we have a proof of some property, we still ought to be able to verify it.

Isn’t verifying a proof equivalent to determining whether a certain computer program halts?

No, but it would be equivalent to verifying that a given computer program halts on a specified N steps.

This is the same distinction between (among other things) P and NP problems. For any problem in P, given an instance of the problem I can produce a solution in polynomial time. For any problem in NP, given an instance of the problem and a candidate solution, I can determine whether the solution is valid in polynomial time.

Determining whether a certain computer program halts would be equivalent to producing a proof, not verifying an existing one.

Verifying a proof is, in principle, only a matter of making sure that each step of the proof is valid. Coming up with the right steps is a creative endeavor. Certainly, coming up with the right set of allowable steps is a creative endeavor, and proving that your system is expressive enough for interesting proofs is a creative endeavor. But once given a proof, verifying that it legally applies legal steeps is a purely mechanical endeavor.

> But once given a proof, verifying that it legally applies legal steps is a purely mechanical endeavor.

But isn't this the same as once having a program then executing it? which then has the problem of does it finish? so back to the halting problem?

No, because a proof (especially a human-constructed proof) is a finite object built out of basic pieces. The only question as to the validity of a proof is whether the basic pieces have been fit together according to the established rules of the game. We don't have to have any notion of "execution" of a proof to verify that its construction is valid.

Let me put it this way. I tell you that I can make apple juice if you give me an apple and a juicer. Do you have to give me anything to believe me?

Several researchers have indeed put together a theory of "execution" of a proof; see for instance Prof. Frank Pfenning's research program on logic-based process calculi. These theories tend to have the common theme of execution as normalization -- the chosen mode of execution actively changes and evolves the proof structure until it reaches a terminal form, usually one with a particularly simple logical structure. Cut elimination is a central theme: any logical system worth calling "computational" (one argues) will support cut elimination, allowing you to replace a proof with steps like `A -> B, B -> C |- A -> C` with a direct proof of `A -> C` that does not use the intermediate hypothesis `B`.

But we're not doing that when we're verifying a proof. We're looking at the finite, static structure of a proof term, and checking that it was put together legally.

The problem with Hilbert’s program was, loosely, that the power to construct propositions was stronger than the power to mechanically check proofs. That is, the formal language of propositional logic + number theory can construct propositions that are not decidable in a finite number of steps.

There are two responses to this discovery: tweak the formal system so you can’t accidentally run into these traps, or shrug and just be more careful about how you prove things.

Now that the world is increasingly computerized, it’s become clear that the right choice is to stop using a default form of mathematical reasoning that causes major issues for mechanized proof assistants and instead build a new foundation that is friendly to computers (but can be extended to support the power of classical formalisms)

Parent is referring to something a bit different - Hilbert’s program was about all of mathematics, even that which hadn’t been discovered yet, whereas the parent is talking about formalizing existing mathematical knowledge in some HoTT-enabled programming language or proof-checker (hence the emphasis on verifying and the problem of siloed knowledge).

Obviously true theorems with existing proofs don’t apply to Godelian incompleteness.