This is exciting news! Though, there is more than just the math that needs to be done here. Namely, mathematicians not only need to formalize a concise language to bridge the gap with modern conformal field theory, but they will also need a way to understand the computability of models based on this system. And yet, there is also the human factor: namely, there needs to be an effort to sell this paradigm to existing theorists, which will require substantial effort.

Can you say more about computability of "conformal models" in the Langlands context (beyond vibes, perhaps cites)? In my understanding, "conformal models" are by construction computable..

Oops, yeah, my bad. I've been doing a deep dive into lean4 and ended up conflating the use of the term computability from that context. Sorry, for the confusion!