My work centers on category theory and its applications to logic and semantics, with a focus on emerging mathematical foundations such as Homotopy Type Theory. I explore the rich interplay between logic, category theory, and algebraic topology, particularly in areas such as synthetic homotopy theory. My favorite tools are internal languages and categorical semantics which enable us to make new bridges between these disciplines. See my publications for more details.
My other major interest is formalization of mathematics in interactive theorem provers, particularly in Lean 4. I am a regular contributor to Mathlib’s category theory library and I’ve been implemeting tools and automation for categories in Lean. My goal is to make Lean a natural and friendly tool for category theory research and teaching.
I currently lead several formalization projects in Lean 4 in areas related to logic, category theory, homotopy theory, and their interplay. If any of these topics interest you, I encourage you to reach out! I am always looking for collaborators and students who are interested in these areas.
I have extensively used Lean in my teaching of math courses, and I am very excited about the ways interactive theorem provers — particularly Lean — are changing how mathematics is learned and taught.
Looking ahead, I’m interested in exploring how interactive theorem proving and automated reasoning can contribute to the development of provably safe AI.
Academic Profile
I earned my PhD in computer science from the University of Birmingham (UK), followed by postdoctoral research positions in mathematics at the University of Leeds, Johns Hopkins University, and Stockholm University.
From 2021 to 2024, I was a postdoctoral research fellow in Emily Riehl’s group at the Department of Mathematics of the Johns Hopkins University. My research focused on the burgeoning field of synthetic homotopy theory, exploring the application of synthetic in simplicial, cubical, equivariant homotopy theory, and K-theory.
From Nov 2019 until Nov 2020, I was a Research Fellow at the University of Leeds Logic group working on the project Univalent type theories: models, equalities, and coherence in collaboration with Nicola Gambino (University of Manchester, formerly at Leeds) and Steve Awodey (Carnegie Mellon University) to develop a Kripke-Joyal style forcing semantics for Homotopy Type Theory. This semantics extends the usual Kripke-Joyal Semantics of Higher Order Intuitionistic Logic in toposes.
I earned my PhD in theoretical computer science under supervision of Steve Vickers. My PhD thesis investigated the bicategorical aspects of classifying toposes arising from the stricter syntactical aspects of a subclass of essentially algebraic theories corresponding to the logic of Arithmetic Universes. My thesis studies point-free generalized spaces (modeled by Grothendieck toposes over varying bases) under the three principles of geometricity, predicativity, and base-independence. It was examined by Peter Johnstone and Martín Escardó.
Before that I was at Western University in London (Canada). I learnt intuitionistic logic and topos theory from John Lane Bell – In fact, I first heard about topos theory and intuitionistic logic in his classical philosophy of mathematics course. I also learnt differential geometry from Martin Pinsonnault.
Short biography
I was born in Qeshm Island in the Persian Gulf in Iran. I have lived in Iran, the Canada, UK, USA, the Netherlands, and Sweden. I speak English, Dutch, and Persian.
Other interests
I started sports in gymnastics (6-12), and later switched to playing football (socccer) as a midfielder. I still play football (soccer) every now and then, but tend to go for trail running more often these days. I am fond of remote places in the mountains, and I go hiking, and remain off-the-grid every now and then.
I am interested in Art history and Architecture and I like to go to museums.
I am an avid reader of philosophy and history and enjoy discussing them. If I had to read one book for the second time, it would be Nietzsche’s Also sprach Zarathustra. The most fun book I have read is Robert Musil’s Der Mann ohne Eigenschaften from 1921. Among mathematician-writers I like to read Haussdorff, Hermann Weyl, and Gian Carlo Rota. The last mathematician who could be claimed to know everything about mathematics was probably Henri Poincaré. Löic Pujet introduced me to Last Thoughts by Poincaré, which was a great fun to read.