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.

lean theorems

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

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".

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

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.

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

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

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).

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 1192: corrected additive-basis energy inequalities, density constraints and campaign history; general target unresolved

Erdos problem #40: for which g(N) -> infinity must a set A with >> sqrt(N)/g(N) elements in {1,...,N} have limsup 1_A*1_A(n) = infinity? Open. Lean: some g works iff the strong form of the Erdos-Turan conjecture holds. Written, after Erdos and Renyi: no power of N works. Computed: the greedy B2[2] set from the #158 thread, to 10,000 terms.