Lean repository linked
The Erdos discrepancy problem
arXiv:1509.05363 · arXiv
Lean formalisations (1)
ProofFleet/prooffleet at 9f6f78688f83
Linked by the repository’s formalization.yaml.
Project review: self-assessed
Audit: awaiting publication.