A lot of areas like real/stochastic analysis are really difficult to map to any formal proving mechanism. Really there are only some areas in abstract algebra w

A lot of areas like real/stochastic analysis are really difficult to map to any formal proving mechanism. Really there are only some areas in abstract algebra where it can be done, and in there you still need some proofs that link a set of real problems to a computable problem and finish with the computation (Groebner basis proofs are one example). But that's rare.