Large language models (LLMs) built on the transformer architecture now produce formally verified proofs of difficult mathematical results, yet we possess only fragments of a mathematical theory of how they represent and manipulate mathematical content. The course treats both objects, the transformer and Lean, as mathematical entities and studies their interaction using the tools of: information theory, Markov processes and their generalizations, high-dimensional geometry, mathematical logic and type theory, and computational complexity. The guiding questions are:

(Q1) What does a transformer compute, in the sense of complexity theory and formal language theory, and how does it encode mathematical concepts?

(Q2) What is the mathematical structure of Lean (type theory, categorical and operadic semantics, decision procedures), and how is that structure reflected in the representations of a language model?

(Q3) Where exactly are the bottlenecks when transformers are coupled to Lean to produce mathematical texts?

(Q4) Are the current transformers the best possible architectures for mathematical texts?

The pace is deliberately slow: every result used is stated precisely and either proved or reduced to a clearly identified result in the literature.