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