Is it possible to use (and how) interactive proof assistants (like Isabelle/HOL, Coq) and automated theorem provers (like E) for proving theorems in analysis and variational calculus and solving differential equations?
As far as I have investigated library for Isabelle/HOL https://www.isa-afp.org/ - then there is no such endeavours. I do not know Mizar - maybe they have such endeavours.
There are efforts to combine computationally creative search and other methods (in the role of human mathematician) (http://ai4reason.org/) with interactive proof assistants and so more or less automate theorem discovery and theorem proving. Currently this is being done for logics, algorithms and discrete math. Is it possible to do this for analysis and if no - then why not?
I can image lot of application arease of such system, especially searching (and automatic investigation) for the optimal models in high energy physics. HEP has very complex models and investigation of each model requires lot of efforts and there is no guarantee that the derived numerical results will be compatiable with the experimental data, so maybe it is possible to automate this trial and error process.
And - if analysis can not be done with IPA/ATP, then maybe it is possible to use IPA/ATP for the handling (discovery and proving) of algorithms that are used for the symbolic manipulation of the formulas of analysis and calculus of variations (e.g. such kind of algorithms that are used in Mathematica).
Added: there is good review presentation http://www.ens-lyon.fr/LIP/AriC/MSC2014/clelay.pdf - Isabelle/HOL has no real analysis, but HOL Light and Coq has almost excellent libraries for this. I would like to stay with Isabelle, so, maybe I should look for Coq theory import in (translation into) Isabelle/HOL? Maybe Isabelle/HOL has analysis through Sledgehammer ecosystem?