I am a postdoc at the University of Alberta, working with Adam Topaz. I obtained my PhD from the University of Copenhagen under the supervision of Dustin Clausen. During my PhD, I worked on establishing the foundations of a theory of solid spectra, a higher analogue of solid abelian groups, a condensed version of complete topological groups, as well as formalizing the foundations of condensed mathematics in the Lean theorem prover. I post my ongoing formalization projects to GitHub. I contribute to Lean's mathematical library mathlib, where I am also a reviewer. I am currently involved in various formalization projects related to category theory, condensed mathematics, and arithmetic and anabelian geometry. My CV is available here.

A formal characterization of discrete condensed objects. arXiv:2410.17847

Categorical foundations of formalized condensed mathematics (joint with R. Brasca, N. Kuhn, F. Nuccio, and A. Topaz). J. Symb. Log. Published online 2024:1-28. doi:10.1017/jsl.2024.69.

Towards solid abelian groups: A formal proof of Nöbeling's theorem. 15th International Conference on Interactive Theorem Proving (ITP 2024), 6:1–6:17. doi:10.4230/LIPIcs.ITP.2024.6.

Palindromes in finite groups and the Explorer-Director game (joint with P. Devlin). Internat. J. Alg. Comput. 31 (2021), no. 3, 491-499. doi:10.1142/S0218196721500235.

PhD thesis: Towards a formalized theory of solid modules. 2025. PhD thesis, University of Copenhagen. Supervisor: Dustin Clausen.

Note: Discrete condensed objects. 2022. Mostly incorporated into my PhD thesis.

Note: Solid spectra. 2022. Mostly incorporated into my PhD thesis. 

MSc thesis: Foundations of condensed mathematics. 2021. Supervisors: Dustin Clausen and Wieslawa Niziol.

M1 thesis: Cranks and t-cores. 2020. Supervisor: Olivier Brunat.

BSc thesis: Palindromes in finite groups. 2019. Supervisors: Pat Devlin and Rögnvaldur Möller. The main results were improved and published in doi:10.1142/S0218196721500235.