Scott Carnahan

Stream: new members

[Scott Carnahan]

Hello everyone!
I'm a mathematician working mostly on vertex algebras and moonshine. I've been starting work on formalizing some theory of vertex algebras, because some of the literature (perhaps including my own work) is a bit cloudy. One concrete but possibly unattainable goal I have in mind is a proof of a 1988 theorem that the symmetries of the monster vertex algebra form a finite simple group.

[Kevin Buzzard]

Hi Scott and welcome!

[Kalle Kytölä]

Hello @Scott Carnahan!

Great to see someone interested in formalizing VOAs! I have secretly had hopes for formalization of VOA theory, partly for the reason that some cloudiness of the literature would definitely be clarified if certain things were formalized, and partly for the simple reason that I care about VOAs in my own research, too.

In fact, for this summer, I got an intern (who had no prior formalization experience but had during the semester taken a course on VOAs) to test the ground for formalizing Dong's lemma (so not yet directly even involving a VOA, but I envision this as a nontrivial test of whether one has a decently working implementation of formal distributions). (And it is not at all given that we'd reach Dong's lemma in the summer!)

[Kalle Kytölä]

I'd be very happy to hear more about your VOA formalization plans! It might even make sense to coordinate a bit, although my own plans in this direction are currently just to test what it takes to have a good enough theory of formal distributions. I at least feel this part is crucial (although very basic); afterwards formalization should either flow naturally (if the formal calculus is set up well) or be absolutely horrible (if the formal calculus is not set up well). One particular design hope of mine is to set up formal series immediately in a generality that later applies also to, e.g., logarithmic intertwining operators (so I would avoid settling just for integer-exponent monomials, or even complex-exponent monomials; I hope the type of monomials can be a pretty general multiplicative monoid; and coefficients of course should be allowed in almost whatever type).

[Scott Carnahan]

Hello @Kalle Kytölä

It is nice to hear from someone with similar interests! My views on developing the theory are essentially in line with yours. I was planning to develop composition of fields roughly following the first 2 sections of Matsuo-Nagatomo's preprint, but with more flexibility in the exponents (lying in some G-set for an additive monoid G) and coefficients (any R-module for a commutative ring R).