The Langlands program is about correspondences between analytic number theory and harmonic analysis. You could think about it as a unification of parts of mathematics that seem to have no reason to join up but turn out to have deep and non-obvious connections. It doesn't have anything to do with formalization.
I thought Stephen Wolfram had already done some victory laps.
You might be thinking of the Langlands program
The Langlands program is about correspondences between analytic number theory and harmonic analysis. You could think about it as a unification of parts of mathematics that seem to have no reason to join up but turn out to have deep and non-obvious connections. It doesn't have anything to do with formalization.
Here's a really good and accessible intro to Langlands https://www.youtube.com/watch?v=4dyytPboqvE
You give me too much credit. I was just being tongue-in-cheek about Principia Mathematica.