Tracking targets in theoretical computer science

The field of theoretical computer science is particularly rich in its use of conjectures. Wikipedia lists [a number of these conjectures and open problems](https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_computer_science). I am putting forward this issue to track some of these that I think would be best suited to inclusion in formal-conjectures, in terms of their importance and ease of formalization.

- [x] P ?= NP (#1120)
- [x] NP ?= co-NP (#1120)
- [ ] [P ?= BPP problem](https://en.wikipedia.org/wiki/P_%3D_BPP_problem) (#5175)
- [ ] [exponential time hypothesis](https://en.wikipedia.org/wiki/Exponential_time_hypothesis) (ETH)
- [ ] The strong exponential time hypothesis
- [ ] Existence of one-way functions
- [x] Is Integer Factorization in P? (#4796)
- [ ] Is Graph Isomorphism in P?