Research

I am interested in the formalisation of mathematics in the Lean proof assistant, especially mathematics related to number theory.

• Formalisation of mathematics in Lean / Mathlib
• Algebraic number theory

Formalisation projects

• Formal Group Laws Formalisation of formal group laws in Lean.
• Robo A game for learning Lean 4, where a smart-elf joins you on your exploration of the Leaniverse. Mentor: Marcus Zibrowius. Work carried out as an AI for Math Summer Fellow.

Preprints and publications

Nothing to list yet.