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?