[proof_by_vibes]

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.

[vinnyvichy]

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..

[proof_by_vibes]

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!