Formalizing superstring perturbation theory

Stream: new members

[Xi Yin]

Hello Lean community!

My name is Xi Yin. I'm a theoretical physicist based at Harvard. I've been pondering about formalizing a proof of the consistency of superstring perturbation theory. While this is not currently established by the standard of mathematics, I think we have understood the necessary recipes through the development of string field theory in the past decade, and a rigorous proof should be attainable with sufficient will and resource.

My experience with Lean so far is limited to playing with AI-generated codes. I realize that currently there is little on Riemann surfaces and Teichmuller spaces in Mathlib, let alone super-Riemann surfaces which would be an essential recipe of the project I'm envisioning. I would like seek advice on how to organize such a project, as well as opportunities for collaboration.

Cheers,
Xi

[Joseph Tooby-Smith]

Hi Xi, We have a project for physics akin to Mathlib called PhysLean, there is a channel on here for it (#PhysLean ). Contributing (the Physics) directly to that project, amongst other things, means that everyone can benefit from everyone else work; and we can have standards amongst the community. Like with Mathlib, the advice would be not to leave this right until the end, as it most likely will never be done.

For what it is worth there is actually some string theory in PhysLean, but on the string-phenomenology side of things - and is related to a paper I'm writing up with Sven Krippendorf.

In terms of organization, my main advice would be to 'organize it like a computer scientist' not a physicist or a mathematician. That means 1. Think about the data structures involved (in physics this could be things like the definition of a Fermion, or a boson etc), and 2. focus on building an API (lots of little lemmas and theorems) around said data structures.

[Xi Yin]

Hi Joseph, thanks, that's good to know!

With a few folks we've been writing Mathematica codes for worldsheet correlator and perturbative string field theory computations, which has already made us think about re-organizing the data structure.

It also occurs to me for string perturbation theory we don't actually need most of the mathematical structures of moduli space of Riemann surfaces, which as I understand would be a substantial challenge to formalize. Rather we only need to deal with integration of certain differential forms on the moduli space, in which case a combinatorial approach e.g. Kontsevich's parameterization via metric ribbon graphs may be sufficient.

My target for formalizing superstring perturbation theory would be to construct the Batalin-Vilkovisky action functional of superstring fields and prove that it satisfies the quantum BV master equation and certain other properties.