# If a human can prove something, can a computer prove it?

I got into a rather intense argument with a friend about to what degree we can expect a completely formalist interpretation of mathematics. Admittedly I don't know very much about the (any of the many) theories of the foundations of mathematics and coming from geometry the idea that everything we currently have (with proofs coming from such a myriad of places, connections with physics, PDEs etc.) could be proved with some sort of finite algorithim is something I can't quite internalise.

Take something where, for instance, the proof is by constructing some sort of pathological example, say the Weierstrass function or something. Now there is a proof of "there exists a function everywhere continuous and almost nowhere differentiable" by simply writing this function down. But since such a function was constructed using mathematical "intuition" and "motivation" I'm not sure what hope, if any, there is to formalize such proofs.

Is it expected any proof given by a person can be found by a finite algorithimic process starting with, say, ZFC and whatever extra bells and whistles that are sometimes thrown in with this? Is it expected that all current proofs in geometry can be given in some sort of reasonable axiomatic system?

• Look into P=NP .. – Quality Nov 8 '17 at 20:49
• Just cause the function took ingenuity to discover doesn't mean the proof that it has those properties isn't formalizable. – spaceisdarkgreen Nov 8 '17 at 20:57
• @spaceisdarkgreen, yes of course checking that the function has the properties is formalizable, but I don't see how an algorithmic process would "invent" such a function, or that there is necessarily some other proof of the fact that a function everywhere continuous and nowhere differentiable exists which would be algortihmic. – R Mary Nov 8 '17 at 21:03
• A proof that the weierstrass function has those properties is a proof that there exists a function with those properties. You want the computer to prove it 'from scratch' which is a tricky concept. Surely we must bestow the computer with some AI / tactics (or with assurance that the proof exists and an unlimited amount of time - see my answer) but how much? If whispering the weierstrass function in its ear is too far, where's the line? – spaceisdarkgreen Nov 8 '17 at 21:25
• Keep in mind that a lot of prominent AI researchers, such as Max Tegmark, believe it is possible that human level artificial intelligence could be created at some point in the future. If that turns out to be correct, then computer programs could become much better than humans at discovering proofs (and every other intellectual endeavor). I think it's fair to say that we don't know the limits of what is possible for artificial intelligence. – eternalGoldenBraid Nov 8 '17 at 21:37