A few years ago, Microsoft researcher Georges Gonthier and INRIA (France) collaborator Benjamin Werner recast the computer-combinatorial proof of the Four-Color Theorem into a logically transparent format Last year, Gonthier and collaborators completed a computer-logical proof of something called the Feit-Thompson Theorm, which has an important role in modern mathematics.
Why might Microsoft be funding this kind of thing?
But the research could also have an impact beyond mathematics. Microsoft hopes to develop a similar system for checking the logic used in computer programs, which could pre-empt some unforeseen bugs that cause programs to crash.(Also, Bill Gates took Harvard's hardest undergraduate math course before he dropped out.)
Abstruse Goose: All math is applied math...eventually.