You may have heard about type theory, either through the world of proof assistants such as Lean or Rocq, or because one of your colleagues was way too enthusiastic about Homotopy Type Theory 10 years ago. Type theories are formal languages used to express mathematics, similarly to more traditional logics, and are often used as foundations for formalization projects. While it might seem that this question of foundations has already been settled for a long time, it is a very dynamic field with many new theories and results, finding applications outside of pure theoretical interest. The goal of this talk is to give a good idea of what research in type theory is like, but also to show what type theory can bring to mathematics beyond being a vehicle for formalization. We will talk about proof assistants and what we want from them, new ways of thinking with synthetic mathematics, and language as an object of study.