[skissane]

> A new "math" might be needed, but an answer (affirming or not) will be found.

What if there exists a proof that P!=NP, but the shortest possible proof of that proposition is a googolplex symbols that long? Then P!=NP would be true, and provable and knowable in theory, yet eternally unprovable and unknowable in practice

[ahmedfromtunis]

That's exactly the kind of situation I had in mind when I wrote that.

Goodstein’s theory would take more symbols than there are atoms in the observable universe to write down in "classic" maths. To "fix" this, mathematicians had to use a "new" way of thinking about infinity known as transfinite induction.

I think if we're smart enough to detect(?) a proof, we'll find a way to express it in a finite manner.