Formal proof
I work on formalized mathematics and reusable Lean interfaces, connecting mathematical results, computable implementations, and proof-system specifications. My public work includes collaborative group-theory research, accepted contributions to mathlib and Verified-zkEVM libraries, and engineering tools for working with Lean. Contribution statuses below were checked on 12 October 2026.
At Harmonic, I formalized IMO-level mathematics and group-theory results, reviewed formal statements and proofs, and contributed to model evaluation and evaluation harnesses for mathematical reasoning and Lean formalization. Ethereum Foundation formalization work in 2026 was through Harmonic.
Kourovka Notebook
With Wouter van Doorn, Pietro Monticone and Daniel Morrison, I co-authored On Some Problems from the Kourovka Notebook, a preprint presenting solutions to eight group-theory problems with Lean formalizations. My contributions include formal proofs and mathematical exposition. The developments are collaborative, and the repository preserves the original Aristotle submissions.
The results concern subgroup structure, ordered products, Rota–Baxter operators and power graphs. For Problem 19.25, the formalization exhibits a simple group and a non-simple group, both of order 6048, with the same element-totient sum, 23984. Thus the order and the sum of Euler’s totient function over element orders do not determine simplicity. For Problem 20.125, the joint development constructs a surjective, non-injective Rota–Baxter operator on a non-abelian group.
The repository also treats Problem 21.149 as formulated in version 43 of the Notebook. This is additional to the paper’s eight results; the stronger formulation in version 45 remains open.
Preprint · Lean formalizations · Paper and collaborators
Selected upstream contributions
Computable polynomial algebra — CompPoly and mathlib
In CompPoly, I contributed interfaces connecting efficient polynomial representations to their mathematical specifications through ring equivalences, coefficient and variable splitting, and evaluation order. Accepted work includes bivariate evaluation, finite-field and KoalaBear lemmas, additive-NTT algebra, and corrections to evaluation assumptions and monic-division early stopping, with regression tests.
I implemented fixed-domain barycentric interpolation with reusable weights, computable handling of evaluation at a node, and correctness against Lagrange evaluation. I also contributed iterative reconstruction; the maintainer subsequently developed its correctness and API theory. These are implementations and reusable proof interfaces for established polynomial algorithms.
Representation and correctness interfaces · Barycentric interpolation — merged February–May 2026. The interpolation source credits Elias Judin and Aristotle (Harmonic).
In mathlib, I generalized the equivalence between single-variable multivariate polynomials and ordinary polynomials from PUnit to any uniquely inhabited index type, preserving compatibility aliases. I added coefficient-transport and evaluation-compatibility lemmas, making the interface reusable across polynomial developments. These contributions were accepted through mathlib’s Bors workflow; the equivalence refactor credits Aristotle for autoformalized proofs.
Equivalence refactor · Coefficient transport
Coding theory — ArkLib
I contributed Johnson-bound counting and inequality proofs, Reed–Solomon proximity-gap results, and correctness and inconsistency properties for the noncomputable Berlekamp–Welch linear-solver specification. The work includes correcting missing hypotheses and degenerate cases. The solver results establish properties of a mathematical specification, rather than verifying an executable Gaussian-elimination implementation.
The AHIV22 development includes proofs of Lemmas 4.3–4.5 and supporting distance, support and counting arguments. Parts of my Guruswami–Sudan work were incorporated through a later upstream development. The source and integration records preserve Aristotle and other contributors’ credit.
Johnson-bound and decoder specifications — merged 26 February 2026 · AHIV22 proximity-gap proofs — merged 24 April 2026
Probabilistic proof interfaces — VCVio and PolyFun
I developed round-by-round probabilistic knowledge interfaces, event games, fresh-challenge bad events, and fixed-context extraction conditions in VCVio. The accepted extraction result is extensional and applies in a fixed context; polynomial-time and asymptotic admissibility require further conditions. State-counting and machine-construction complexity proofs were incorporated into PolyFun’s complexity backend and VCVio through later integrations.
Knowledge and extraction interfaces — merged 27 July 2026 · PolyFun integration
I also contributed random-oracle query-budget tests and product-extraction countermodels separating binding, component soundness and relation refinement. They check cache consistency and fresh-query independence and exercise the relation-refinement conditions required for product extraction. A maintainer incorporated my tests alongside their own new library lemmas.
Test integration and attribution — merged 23 September 2026
Proof-system algebra — leanerVM
I contributed coefficient transport and mixed-ring evaluation for aligned polynomial stacks, arbitrary-column readout and pairing, and padding-aware multilinear identities. Public index and bytecode-column evaluators come with correctness proofs and boundary tests, including the relevant bit-order and program-input conditions.
Integrated upstream alongside other contributors’ modules, with maintainer reorganization and generalization, these algebraic foundations support protocol proofs. The integration explicitly credits Elias Judin, Stefano and Aristotle.
Upstream integration and contributor credits — merged 29 September 2026
Polynomial interpretation — Clean
I contributed polynomial interpretations of Clean expressions with evaluation agreement and degree bounds. The finite-width interpretation requires in-range variables for array-backed evaluation.
Polynomial interpretation — merged 5 October 2026
Tools for working with Lean
lean-lsp-mcp
I made sustained reliability contributions to this Python MCP server connecting AI agents to Lean: temporary-proof lifecycle, concurrent-client startup and teardown, UTF-16 ranges, project-root discovery, bounded and non-blocking search, process handling, and project-boundary and authentication checks. I added regression tests and refined the changes with the maintainer.
Contribution and maintainer review — merged 8 April 2026
lean4-skills
I contributed a native Codex adapter reusing the existing Lean skill tree, with host-aware hooks, runtime diagnostics, release checks and cross-platform tests.
Native adapter contribution — merged 3 August 2026
Submission status
The ArkLib round-polynomial submission remains open. It identifies honest sumcheck-round polynomials with their projected polynomial expressions over commutative semirings, including finite and trivial ones.
The leanerVM sumcheck submission was closed without merging on 6 October 2026.