Hacker News Reader

Comment by joe_the_user | Hacker News Reader

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.

View on HN

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 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.

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:)).

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

Reply on news.ycombinator.com