1
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ Look into P=NP .. $\endgroup$ – Quality Nov 8 '17 at 20:49
  • 1
    $\begingroup$ Just cause the function took ingenuity to discover doesn't mean the proof that it has those properties isn't formalizable. $\endgroup$ – spaceisdarkgreen Nov 8 '17 at 20:57
  • $\begingroup$ @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. $\endgroup$ – R Mary Nov 8 '17 at 21:03
  • $\begingroup$ 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? $\endgroup$ – spaceisdarkgreen Nov 8 '17 at 21:25
  • $\begingroup$ 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. $\endgroup$ – eternalGoldenBraid Nov 8 '17 at 21:37
3
$\begingroup$

It is believed that (effectively) all classical mathematical theorems and their proofs can be mapped to theorems and proofs in ZFC. These proofs could be verified by a computer but we wouldn't require the computer to come up with the steps of the argument by itself in order for the proof to be formalized, just that it verify them.

This is not to say that there isn't any interest in or progress with having computers actually attempt to automatically generate a proof on its own... this is an active field. And in a narrow sense a computer can always do this. It can simply enumerate all possible proofs. If the theorem has a proof, it will eventually spit it out.

This is obviously not feasible in real life. And it also only works if we know there is a proof. Otherwise the computer will keep enumerating the proofs and we won't be able to tell if the proof of the statement in question doesn't exist or is simply not one we've enumerated yet. We could get clever and look for proofs of its negation in parallel, but by Godel's theorem there are statements such that neither they nor their negation are provable.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.