Abstract
After a brief explanation of how language models work, we will explore their application to mathematical reasoning, in particular their ability to produce informal mathematical reasoning as well as formal proofs. We will discuss the trade-offs involved in generating informal and formal proofs, the inherent limitations of large language models in these two modalities, as well as potential future directions for overcoming these limitations. We will also examine the use of these language models at the intersection of these two modalities, in particular, their use for self-formalization.
