: Mathematician & AI engineer : category theory : universal algebra : topology & sheaf theory : formal verification : foundation-model infrastructure :
now
now: may 2025 — Lean4 formalization (part-time), march 2025 — AMC/AIME Lean4 labeling, august 2024 — Weekly category seminars, march 2024 — Research grant 2024
:: may 2025 — Lean4 formalization (part-time) :: march 2025 — AMC/AIME Lean4 labeling :: august 2024 — Weekly category seminars :: march 2024 — Research grant 2024 ::
affiliations
affiliations: Harmonic, Project Numina, University of Cape Town, University of the Witwatersrand, Kili Technology, Lean Prover community, SAMS
::: Harmonic ::: Project Numina ::: University of Cape Town ::: University of the Witwatersrand ::: Kili Technology ::: Lean Prover community ::: SAMS :::
Mathematics Research Blog
Articles on category theory, universal algebra, topology, and the cultures around mathematics.
Exercises in category theory: how modules over a ring and vector spaces over a field can be framed as algebraic categories by extending the operator signatures to handle scalar multiplication.
Monoids and preorders as categories: characterize when they are groupoids (groups/equivalence relations) and when they are skeletons (orders). With examples.
Using Tokieda’s overflow heuristic and isotopy in R^3, show the double-twisted Mobius strip cannot isotope to the ordinary strip (Hopf link obstruction).