Large language models (LLMs) are advancing the state of the art in nearly all areas of artificial intelligence, yet they remain poorly understood. At a time when new abilities as well as new limitations of LLMs are continually coming to light, a clear understanding of what they can and cannot do (that is, their expressivity) is becoming increasingly important. Furthermore, differentiating between the tasks that LLMs can solve at all scales, and those that LLMs can solve at small scales but are guaranteed to fail on at larger scales can be central to the success of some applications of LLMs, particularly where safety guarantees are needed. These questions can be answered with certainty only by mathematical verification. This project is contributing to the study of connections between LLM expressivity and mathematical logic. It is using those connections to reap both theoretical and practical benefits, in the form of new guarantees for LLMs, new extensions of LLMs, new methods for explaining how LLMs work, as well as new developments in mathematical logic. Just as the Curry-Howard isomorphism established a deep connection between logic and programming languages that enabled many results to be exchanged between the two fields, we are developing a "Curry-Howard isomorphism for neural networks": not merely a connection between one kind of neural network and one logic, but a correspondence between the elements of neural networks and the elements of logic that leads to a rich exc