: 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 :::
Honours project on free semimodules and their examples. Covers definitions, universal properties, and connections to category theory and universal algebra. Supervised by Prof. G. Janelidze (UCT).
Free algebras as initial objects in C[X]. Example: free vector spaces; the universal-property definition also yields free magmas, free groups, and more.
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.