Algorithms and Complexity Theory

Stream: Formal conjectures

[Bolton Bailey]

There are a lot open problems in computer science, and it might be nice to add some to the formal conjectures project. I am thinking in particular of problems like:

• In complexity theory
  • P vs NP
  • P vs BPP
  • P vs PSPACE
  • ETH/SETH
• In algorithms
  • Is Integer factorization in P
  • Is Graph Isomorphism in P

Unfortunately, I don't think Mathlib currently has a definition for the notion of complexity classes, but I think it would not be too hard to make one and define a few basic complexity classes. What are peoples thoughts on the following questions:

• Do questions about algorithms belong in formal-conjectures?
• Do questions about complexity classes belong in formal-conjectures?
• If we do want problems about complexity classes, should we attempt to add the concept of complexity classes to mathlib first so that the definitions don't need to be placed in the formal conjectures repository?
• Alternatively, should we try to add these definitions to the relatively new CSLib project and add a dependency on that?

[Anirudh Rao]

I think algorithmic questions and complexity classes should definitely be in formal-conjectures! I don't see why we couldn't just put those definitions in the repo for now and then add them upstream to Mathlib/CSLib later.

[Moritz Firsching]

Bolton Bailey said:

• Do questions about algorithms belong in formal-conjectures?
• Do questions about complexity classes belong in formal-conjectures?
• If we do want problems about complexity classes, should we attempt to add the concept of complexity classes to mathlib first so that the definitions don't need to be placed in the formal conjectures repository?
• Alternatively, should we try to add these definitions to the relatively new CSLib project and add a dependency on that?

Very generally I would vote for having open problems in computer science included in the formal-conjectures repo -- seems like it is more of a spectrum. We already have questions that go more towards the computer science direction, for instance https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Other/BeaverMathOlympiad.lean

The stuff you proposed could make great contributions!
I'm not sure if we want to add the corresponding definitions/api to our ForMathlib first or if we should introduce a ForCSLib and later also depend on it, I suppose it depends on what exactly will be added. I don't think there are strong reasons not to add a dependency to CSLib when needed.

[Bolton Bailey]

Perhaps the best way would be to simply add it to ForMathlib in a ComplexityTheory folder, with the idea that it could eventually be upstreamed to either repo, depending on how their scope evolves.

[Bolton Bailey]

https://github.com/google-deepmind/formal-conjectures/issues/676