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. The paper distinguishes Aristotle’s discovery and initial Lean proofs from the authors’ work on problem selection, statement clarification, mathematical exposition and reusable formal infrastructure. We refined and reorganized the formal developments partly by hand and partly with Aristotle. The repository preserves the original 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. The submissions include proofs autoformalized by Aristotle (Harmonic).
Representation and correctness interfaces · Barycentric interpolation — merged February–May 2026. The interpolation source credits Elias Judin and Aristotle (Harmonic).
Further contribution records: KoalaBear and additive NTT proofs · Bivariate coefficient and evaluation bridges · Monic division correction · Variable splitting · Iterative reconstruction submission and dhsorens’s subsequent development.
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 · Evaluation API parity
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 Johnson-bound, solver and AHIV22 submissions include proofs autoformalized by Aristotle (Harmonic). 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 proofs — merged 26 February 2026 · AHIV22 proximity-gap proofs — merged 24 April 2026 · Solver solution correctness · Solver inconsistency · Guruswami–Sudan submission and MavenRain’s subsequent development
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 submission credits Aristotle (Harmonic) as a co-author. The accepted extraction result is extensional and applies in a fixed context; polynomial-time and asymptotic admissibility require further conditions. My state-counting proof contributions, with proofs generated by Aristotle (Harmonic), were carried through Devon Tuma’s VCVio development into Quang Dao’s PolyFun integration. These are contributions to the larger complexity development.
Knowledge and extraction interfaces — merged 27 July 2026 · PolyFun integration · Original proof contribution · Intermediate development and provenance
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. Quang Dao incorporated my tests alongside new library lemmas. The random-oracle controls derive from work credited to Stefano Rocca, Aristotle (Harmonic) and me; the product-relation countermodels are a separate submission.
Test integration and attribution · Random-oracle controls · Product-relation countermodels — 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, extending the earlier zero-padding formula to arbitrary padding. 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. Scaraven’s integration preserves the joint source credit to Elias Judin, Stefano Rocca and Aristotle (Harmonic), and distinguishes the earlier submissions from its subsequent changes.
Upstream integration and contributor credits · Coefficient transport · Arbitrary-column claims · Arbitrary padding · Public-column evaluators — 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.
Path policy and authentication — merged 8 April 2026 · Snippet lifecycle · Concurrent startup and UTF-16 · Search project root · Bounded search · Non-blocking tools · Transport handling · Teardown · Verification lifecycle
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.