I will discuss a dictionary between the quantities in the
spectrum of the string theory compactified on the Calabi-Yau and
object in the Calabi-Yau. I will also discuss some properties.
A few months ago, I decide to attempt to formalize one of my own
papers using the Lean4 theorem prover. I will report on this
experiment. (The Lean code can be found there: https://github.com/smorel394/TS1)
A $\mathrm{GL}$-variety $X$ is an (infinite-dimensional) affine
variety with an action of the infinite general linear group
$\mathrm{GL}$ such that the coordinate ring of $X$ is a
polynomial $\mathrm{GL}$-representation and generated by
finitely...
