It's especially interesting given that P vs NP is suspected to be unprovable in ZFC. Waiting for further development!
What would make mathematicians suspect that (if you know)? I mean ZFC is not a toy system, it is obviously used in complex and deep ways to prove or resolve long-standing questions in ways that build on tons of deep results that themselves took tons of research. (By the way for anyone else reading, just so you don't get the wrong idea: ZFC is actually the standard set of axioms mathematicians work with every day. It's the normal way to do math.)
What would make someone suspect this one is impossible to prove/decide under ZFC? (Or what would make someone think it is independent under ZFC?)
"A lot of people have tried to prove it" doesn't seem a convincing argument. (Consider advances toward the twin prime conjecture, or the now-proven Fermat's last theorem, etc.) There must be something more that makes you say that.
Thank you for any answer.
I'd dispute that mathematicians work with ZFC every day. Most pure but not foundational mathematics basically works with intuitionist set theory. By keeping the size and nesting of sets small enough, we never need to worry about ZFC.
Zorn's lemma comes up occasionally, but that is all.
What my parenthetical comment that you quoted meant to say (for anyone that was not familiar with it) is thaz ZFC is not some joke, or obscure set of axioms or something irrelevant. Without this remark I thought my comment read that way.
I hope you will agree that ZFC is simply "standard math" - even if its axioms are not referenced explicitly by many working mathematicians.
If this statement requires further refinement let me know. Obviously I'm not a mathematician!
My point was that foundational mathematics is rarely touched upon by a lot of normal pure mathematics (say number theory, field extension, graph theory).
Interestingly, I believe a lot of people actually dislike the axiom of choice. They find it to be way to 'complex' when compared to the other axioms. It is a lot like euler's 5-th axiom (2 straight lines with the same direction are equidistant everywhere). Interestingly in that case, removing the axiom led to spherical and hyperbolic geometry.