Efforts in Algorithms and complexity

Stream: computer science

[Izan Beltran]

Hello! Is there any established effort on formalizing algorithms and their time & memory complexity? And complexity theory in general? Thanks a lot!

[Fabrizio Montesi]

@Shreyas Srinivas had some interesting comments about it.

[Izan Beltran]

Where I can find these messages?

[steven kelk]

Hi everyone, I'm also interested in efforts to formalize mathematics (and assisted/automated theorem proving) in the area of algorithms and complexity, because that's where I work. I know it is not fashionable but, in particular, I find NP-hardness proofs a particularly interesting lens through which to monitor these developments. In algorithms and complexity NP-hardness proofs often induce an eye-rolling response from those who mainly focus on positive results, due to being mundane and/or pessimistic. For these reasons it is very hard to publish NP-hardness results these days, unless they are stupendously complex or deep (in which case, good luck finding the reviewers to check them) or they are a small part of a wider array of results. But they remain beautiful proofs, in my humble opinion, and they seem to require a very large degree of creativity to produce (such as the design of exotic 'gadgets'). There are countless examplesof such proofs, but other than some general design principles there don't seem to be any axioms or suchlike which help guide the mathematician from the empty sheet of paper to the final result. For all these reasons I really consider NP-hardness proofs as very important test cases for developments in this area!

[Anthony Wang]

I'd say that NP-hardness proofs are not as respected in theoretical CS is that it's simply quite easy to create or find new problems and prove them to be NP-hard. For instance, two years ago I took an MIT class about NP-hardness (and complexity theory more generally) and a large portion of the problems we solved in class were open problems about various games such as Super Mario Bros that most researchers don't care about. I do agree that these proofs often require a lot of creativity but that also means they tend to be very ad-hoc and probably wouldn't belong in cslib. As for formalizing NP-hardness proofs in Lean, usually these proofs are polynomial-time reductions to 3-SAT. However, I don't think the Cook-Levin theorem has been formalized in Lean yet, although it has been in Rocq, so most of the work would probably be to prove the Cook-Levin theorem and then the reduction from 3-SAT to SAT. Additionally, there isn't a consensus yet how to formalize time complexity in cslib, and thus polynomial-time reductions as well.

[Anthony Wang]

So in short, cslib is probably not ready yet for doing NP-hardness proofs.

[steven kelk]

Hi Anthony,

Thanks for the response!

I'm drifting a bit off-topic here (towards automated proof) but for what it's worth:

1. I agree that the ability to dream up new problems (which you then prove hard) are one reason for many people not being interested in NP-hardness proofs. However, things become more interesting if a problem has been around for sometime and attracted reasonable interest but its complexity
   remain unresolved. There are many such open complexity questions in the literature. At the point mechanization/automation can crack such a proof, I will be extremely impressed; this will be a game-changer for me.

2. It's true that many NP-hardness reductions reduce from (3-)SAT... but a great many do not. Many complexity results in the applied mathematics literature tend to reduce from other NP-hardness problems, simply because the effort to reduce a 3-SAT instance into unusual problem X can be huge (for a human...). And, indeed, part of the art of NP-hardness proofs is knowing which NP-hardness problem Y to reduce from, in order to make life bearable. [Of course, you then assume that the original NP-hardness reduction for Y was correct]. So the creative challenges in proving NP-hardness are amongst others, (I) is it actually NP-hard at all? Why do we exclude the existence of a polynomial-time algorithm? (2) What problem should we reduce from? (3) How on earth
   do we build the appropriate gadgets?

Cheers,

Steven