I think that this is being used to verify results notably the Kepler conjecture by the Flyspeck project. So this is now one way to try to prove theorems and thus is of interest to practicing mathematicians.