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?
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.