Yes, there are non-constructive proofs for the existence of polynomial time algorithms [1]. The Robertson–Seymour theorem [2] is a common example, it shows that

Yes, there are non-constructive proofs for the existence of polynomial time algorithms [1]. The Robertson–Seymour theorem [2] is a common example, it shows that certain classes of graphs can be characterized by finite sets of forbidden subgraphs [3] which can be checked for in polynomial time but it does say what those sets of forbidden subgraphs are or how they can be found. [1] https://en.wikipedia.org/wiki/Non-constructive_algorithm_existence_proofs https://en.wikipedia.org/wiki/Non-constructive_algorithm_exi... [2] https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo... [3] More precisely forbidden minors.