My work sits at the intersection of machine learning for formal reasoning, formal methods (automated and interactive theorem proving), and category theory. I come to this from categorical logic and Homotopy Type Theory, where internal languages and categorical semantics have been my favorite tools for building bridges between logic, category theory, and algebraic topology, particularly in synthetic homotopy theory. See my publications for more details.

I am currently a senior research associate at the University of Cambridge working on machine learning for automated theorem proving in Jamie Vicary’s group.

Previously, in 2024–25, I was a Lean expert at Harmonic AI.

I currently lead several formalization projects in Lean 4 in areas related to logic, category theory, homotopy theory, machine learning, and their interplay. With Steve Awodey, I co-lead HoTTLean, a deep embedding of Homotopy Type Theory in Lean 4, together with a formalization of its meta-theory. Its certifying type checker lets one write synthetic proofs in HoTT and soundly transfer them to classical statements about, for example, groupoids. As a next stage, we are considering an AI proof-search agent inside HoTTLean, to test whether machine provers reason better in a synthetic language such as HoTT than in classical Lean. HoTT also becomes a natural target language for autoformalization: parallel proofs in HoTT and in Mathlib would give a dataset for training models that translate between the HoTT libraries of Rocq and Agda and Lean’s Mathlib.

My other major interest is formalization of mathematics in interactive theorem provers, particularly in Lean 4. I am a regular contributor to, and reviewer for, Mathlib’s category theory library, where my contributions include condensed mathematics, cohomology theory, weak factorization systems, and locally cartesian closed categories. I’ve also been implementing tools and automation for categories in Lean, and in 2024 I formalized the theory of polynomial functors in maximal generality. My goal is to make Lean a natural and friendly tool for category theory research and teaching.

I have extensively used Lean in my teaching of math courses. At Johns Hopkins I redesigned Introduction to Proofs, integrating Lean, and in Fall 2023 added machine learning to the course: students generated conjectures with neural networks, tested them in Lean, and corrected AI-generated proofs. I am very excited about the ways interactive theorem provers — particularly Lean — are changing how mathematics is learned and taught.

Looking ahead, I am interested in trustworthy and modular autoformalization. As AI agents generate ever longer formal proofs, it becomes harder to check that the formal statements say what the informal mathematics says, especially when agents write ad-hoc definitions instead of building on libraries such as Mathlib. I would like to explore decomposing autoformalization into independently checkable modules at different levels of abstraction, with category theory and synthetic mathematics as organizing tools.

More broadly, I’m interested in 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.

I started sports in gymnastics (6-12), and later switched to playing football (soccer) as a midfielder. I 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 also 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.