Formal proof
My formalization work in Lean spans group theory, computable polynomial algebra, coding theory, and the mathematics of proof systems. This page collects a joint research paper, selected upstream contributions, and ongoing projects. Contribution statuses were checked on 28 September 2026.
Kourovka Notebook
With Wouter van Doorn, Pietro Monticone, and Daniel Morrison, I co-authored On Some Problems from the Kourovka Notebook, presenting solutions to eight group-theory problems with accompanying Lean formalizations. The results concern subgroup structure, ordered products, Rota–Baxter operators, and power graphs, among other topics.
For Problem 19.25, the formalization gives a simple group and a non-simple group, both of order 6048, with the same element-totient sum, 23984. Thus a finite group’s order and the sum of Euler’s totient function over its element orders do not determine whether it is simple.
For Problem 20.125, the joint development constructs a surjective, non-injective Rota–Baxter operator on a non-abelian group. The witness is the product of the symmetric group on three letters with the group of integer sequences; the operator inverts the permutation and shifts the sequence.
The repository also treats the original formulation of Problem 21.149. This is separate from the paper’s eight results: the strengthened formulation in version 45 of the Notebook remains open.
Paper and collaborators · arXiv · Lean development
Selected upstream contributions
Coding theory — ArkLib
Proofs of AHIV22 Lemmas 4.3–4.5 in ArkLib’s proximity-gap development, with supporting arguments about distances, supports, and counting. These discharge the proof obligations for the three lemmas used in that development.
Contribution and proofs · merged 24 April 2026.
Polynomial computation — CompPoly
A computable barycentric evaluator for repeated interpolation queries on a fixed set of distinct nodes over a field, with precomputed weights. The correctness proofs identify its output with Lagrange interpolation. An explicit node-hit case handles evaluation at an interpolation node, where the usual rational expression would have a zero denominator.
Contribution and proofs · merged 20 May 2026.
Random oracles and extraction — VCVio
Random-oracle controls establish cache consistency, independence for fresh queries, and the exact difference between guessing with zero and one hash query. Separate sampled Boolean countermodels show why component soundness alone does not supply the relation-refinement obligations needed for product extraction, even with a fixed extractor and perfect binding.
My contributions in #767 and #768 were incorporated as tests through a maintainer’s PR, #784, alongside new library lemmas. The countermodels identify missing premises; they do not establish a general product-extraction theorem.
Random-oracle controls · Extraction controls · Upstream integration, merged 23 September 2026.
Ongoing research
Polynomial interfaces for leanVM-related proofs
This work connects polynomial representations, sumcheck rounds, and committed-column and stacking interfaces across Lean libraries. Current submissions include interpreting Clean expressions as polynomials with evaluation agreement and degree bounds, and identifying honest sumcheck round polynomials with their projected polynomial expressions. The latter identities hold over commutative semirings, including finite and trivial ones.
These are contributions to the algebra and interfaces supporting protocol proofs. The submissions linked here remain under review; they do not establish complete VM verification or end-to-end protocol security.
Clean polynomial interpretation · ArkLib round-polynomial identities · leanerVM sumcheck connection
Burnside101
An ongoing reconstruction of the Novikov–Adian argument in Lean. The main branch contains free Burnside group foundations, including the universal factorization property, and a rank-one development of Adian’s 2015 modification: periodicity, minimization, continuation, replacement, and reversal constructions.
The rank-one results are partial progress. Higher-rank arguments and the infinitude theorem for odd exponents at least 101 remain unfinished.
Methods and background
The Kourovka project used Aristotle, Harmonic’s formal reasoning agent, to discover solutions and produce Lean proofs. The ArkLib proximity-gap and CompPoly interpolation contributions above also credit Aristotle for autoformalized proofs. The linked papers, source headers, and contribution records give the attribution for each development.