Every math paper ever (there are about 4 million of them) will get formalized. One benefit of this is finding out which ones were actually correct, and which had unrecognized flaws in their claimed results.

After that, we can do statistics to see which ideas in math are most used, and perhaps mine for unrecognized patterns, refactoring math to find new abstractions.