I am a researcher in category theory, type theory, logic, interactive theorem proving and formalization of mathematics. I work on the interplay of logic, category theory, and algebraic topology, such as in synthetic homotopy theory. I have studied topos theory, internal languages and categorical semantics to enhance our understanding of the relationships between logic, type theory and homotopy theory, and make new bridges between these disciplines.

I am also a user of Lean4, a formalizer of category theory in Lean, a contributor to mathlib.

Currently I am implementing geometric deep learning algorithms in Lean 4.

Academic Profile

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 grew up in Iran, I have lived in the Canada, UK, USA, and the Netherlands. I speak English, Dutch, and Persian.

Other interests

Started in gymnastics (6-12), and later switched to playing football as a midfielder. The sport I like to watch is free-style wrestling.

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.

The best novel I have read is Robert Musil’s Der Mann ohne Eigenschaften from 1921. Musil’s wit is unsurpassable, and he understood the human condition in modernity like no other being.