Curriculum Vitae
Profile
Mathematician working in categorical algebra and Lean formalization, with experience in model evaluation and evaluation harnesses for mathematical reasoning. Based in Cape Town, South Africa.
Professional Experience
Theorem Proving Engineer — Harmonic · May 2025–August 2026
Remote, part-time contract.
- Worked on Lean 4 formalizations of IMO-level mathematics and group-theory results. Reviewed formal statements and proofs.
- Contributed to model evaluation and harnesses for mathematical reasoning and Lean formalization.
- Worked on Ethereum Foundation formalization through Harmonic in 2026.
Theorem Proving Engineer — Project Numina · March–May 2025
Via Kili Technology; remote, part-time.
Formalized AIME-level problems in Lean 4 and mathlib, and reviewed statements and proofs.
Publications and Preprints
On Some Problems from the Kourovka Notebook · 2026
Wouter van Doorn, Elias Judin, Pietro Monticone and Daniel Morrison. Preprint presenting solutions to eight group-theory problems with Lean formalizations. Contribution: formal proofs and mathematical exposition.
Paper and collaborators · Lean source
Education
MSc Mathematics — University of Cape Town · 2023–present
Thesis in progress: Semirings, Semimodules, and Semialgebras. Supervisors: George Janelidze and Juana Sánchez-Ortega.
BSc Honours Mathematics — University of Cape Town · 2022
Cum laude (89%); conferred March 2023. Project: Free Semimodules and Their Examples. Supervisor: George Janelidze.
BSc Mathematics and Computer Science · 2019–2021
University of the Witwatersrand; cum laude.
Teaching Experience
UCT tutoring and marking: Linear Algebra and Fundamentals of Mathematics (2023); Introduction to Discrete Mathematics (2022).
Wits tutoring: Discrete Computational Structures (2021).
Honours and Awards
UCT Master’s bursary through the Building Research Active Academic Staff Grant (2023–2024). Myer Levinson (EMDIN) Scholar (2022–2024). Wits Dean’s List and University Council Merit Scholarship (2020, 2021).
Summer Schools
New Horizons in Theoretical Computer Science (31 May–4 June 2021). Organizer: Boaz Barak.
IBM Qiskit Global Summer School, Certificate of Quantum Excellence (July 2020).
WitsQ-IBM Quantum Computing Summer School (December 2019).
Formal Verification Projects
Selected collaborative contributions to Verified-zkEVM and mathlib. Some formalizations used Aristotle (Harmonic). The Formal Proof page gives mathematical details, sources, and contribution statuses.
Computable polynomial algebra — CompPoly and mathlib
Contributed polynomial representation equivalences and correctness interfaces, bivariate evaluation, finite-field and additive-NTT lemmas, and fixed-domain barycentric interpolation. Corrected evaluation assumptions and monic-division early stopping, with regression tests. Extended mathlib’s single-variable polynomial equivalence and coefficient/evaluation APIs.
CompPoly contributions · Barycentric interpolation
Coding theory — ArkLib
Contributed Johnson-bound and Reed–Solomon proximity-gap formalizations, correcting missing hypotheses and degenerate cases. Added correctness and inconsistency proofs for the noncomputable Berlekamp–Welch linear-solver specification. Parts of the Guruswami–Sudan work were incorporated upstream.
Johnson-bound and decoder specifications · Proximity-gap proofs
Probabilistic proof interfaces — VCVio and PolyFun
Contributed round-by-round extraction and probabilistic knowledge-transition interfaces, random-oracle query-budget tests and countermodels separating binding, component soundness and relation refinement. Machine-counting and state-normalization proof contributions were incorporated into PolyFun’s complexity backend.
Knowledge and extraction interfaces · PolyFun integration
Proof-system algebra — leanerVM
Contributed mixed-ring evaluation of aligned stacks, padding-aware multilinear identities, and public index and bytecode-column evaluators with correctness proofs and boundary tests. Integrated upstream alongside other contributors’ modules.
Upstream integration and contributor credits
Software Engineering Projects
lean-lsp-mcp — Python MCP server connecting AI agents to Lean
Contributed improvements to concurrent-client startup, UTF-16 ranges, non-blocking search, process handling, and project-boundary and authentication checks. Added regression tests and refined changes with the maintainer.
Contribution and maintainer review
lean4-skills — Native Codex adapter
Contributed host-aware hooks, runtime diagnostics, release checks and cross-platform tests, reusing the existing Lean skill tree.
Academic Activities
Participant in UCT’s Category Theory Seminar.