[Virginia-American]

Is it known that there are provable theorems out there that are hopelessly beyond the human intellect to prove?

Consider the four-color theorem. The original proof requires the use of a computer to check billions of cases; here's a link to another proof, where the author says

"The first proof needs a computer. The second can be checked by hand in a few months, or, using a computer, it can be verified in about 20 minutes."

As a general rule, given any formal system, and given any positive N, there will be theorems in it whose proof requires at least N steps. That's any N - eg 10 to the 10 to the 10 ... to the 10.

[Physicist]

Consider the four-color theorem. The original proof requires the use of a computer to check billions of cases

I maintain that computer programs are implementations of human reasoning, thus all of their results fall under that heading.

[LibWhacker]

As a general rule, given any formal system, and given any positive N, there will be theorems in it whose proof requires at least N steps. That's any N - eg 10 to the 10 to the 10 ... to the 10.

In other words, there are proofs that require an infinite number of steps? That's the immediate implication.

I guess it'd help me if I understood whether we are talking about proofs in general or only about algorithmic "proofs." It's true that there are brute force proofs which take a huge number of steps to check every case, but of course that doesn't imply that more "elegant" solutions don't exist. The four-color theorem may be a case in point.