: 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.
Notes on topological, lax-topological (semi-topological/solid), and topologically algebraic functors via structured sources/sinks, classical characterizations, and the quantaloid-enriched “topological = total” theorem.
Speculative essay on Meillassoux’s arche-fossil, Simone Weil’s attention, and whether AI-generated mathematics could signal an ancestral truth that exists beyond human understanding while still demanding translation back into meaning for us.
Notes on Alfred Tarski’s 1966 lecture “What are logical notions?” and his proposal that logical notions are precisely those invariant under all automorphisms of the universe of discourse, with references for further reading.
Short primer explaining presheaves, the locality and gluing axioms, and the equalizer diagram that packages the sheaf condition for a topological space.
Hom-sets worked out in any category: hom-functors preserve identities and composition, and detect monos/epis by injectivity - notes for Lean 4 formalisation.
A guide to describing and visualizing complex topological spaces such as tori, Klein bottles, and Möbius strips using gluing diagrams and geometric intuition. Explores identification spaces.
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).
Yoneda lemma for monoids via M-sets: explicit Nat(M(-), X) <-> X bijection, Cayley as a corollary, plus Yoneda embedding and an enriched remark for self-study.
Free algebras as initial objects in C[X]. Example: free vector spaces; the universal-property definition also yields free magmas, free groups, and more.