MachineChecked

Lean repository linked

Proof of the Erdős-Szemerédi sunflower conjecture

Matija Bucić, Fankang He, Hyunwoo Lee · 2026

arXiv:2610.26686 · arXiv

Lean formalisations (1)

mbucic4/erdos-szemeredi-sunflowers at 8b5dc7ba9fa9

Linked by the repository’s formalization.yaml.

Project review: agent-reviewed; independently kernel-checked

Audit: awaiting publication.

Report this listing