The material linked to from this page is about automating mathematics by formal proof (together with references to pages for automating mathematics and and proof separately).
In some cases, technology intended for just one of these areas may nevertheless be suitable for the combination.
Mizar and Automath are both systems which have been used extensively for developing machine checked formal proofs in a variety of branches of mathematics.
The QED project is as yet more aspiration than reality.
The aspiration includes the computerised formalisation of substantial parts of mathematics.
All of these projects seem to be concerned primarily with the development rather than the application of mathematics, where proof is traditionally thought most relevant.
The possibility of using logic for problem solving in applied mathematics has so far attracted little interest.
