additive-combinatorics

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

Formalisation of the Kelley-Meka bound on Roth numbers

The sublibrary of Mathlib dedicated to additive combinatorics

Miscellaneous projects I am working on in Lean

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

AddComb.js is a javascript library for additive combinatorics calculation.

Executable certificate framework for a proof candidate of Graham’s rearrangement conjecture / Erdős #475, with local branch checkers and reproducible audit scripts.

Official Python/SageMath implementation and numerical verification suite for Sun's (2,4,6,8) Binomial Representation Conjecture (Framework V10.3).

Mini research lab for 3-player Number-on-Forehead Exactly-N: corner-free sets from Behrend-style construction, certificate verification, parameter sweeps, and reproducible outputs.

lean theorems

Behrend’s construction relies on the idea that points on the surface of a high-dimensional sphere cannot contain arithmetic progressions (or corners) because the sphere is "curved".

Exact extremal-set classifications over F31 and F73: sum, product and progression avoidance; original C/C++ and Python verification

Experimental lab for Gowers grid norms ∥ f ∥ G ( k , ℓ ) ∥f∥ G(k,ℓ) ​ on 2D masks—box norms, exact G ( 2 , k ) G(2,k) scans, Behrend + corner-free x + 2 y x+2y lifts, and README figures, motivated by arXiv:2504.07006 (corners theorem).

Erdős problem 142 research notebook — OPEN (single final obstruction). Audits, verifiers, roadmap. © Mangesh Raut

Automating the Markov chain method from Tao et al. (2026) for Erdős primitive set conjectures (arXiv:2605.00301)

Computational research notebook for Erdős Problem 124, including the multi-base Bernoulli convolution AC conjecture and C++ triple-check.

Certified global lower-bound improvement for the Erdos minimum-overlap problem: c_E > 0.38055925 via independent Arb and MPFI checks; the exact value remains open.

Erdos 39: formal Sidon density bounds, infinite greedy construction, computational controls and original receipts

Erdos 1192: corrected additive-basis energy inequalities, density constraints and campaign history; general target unresolved