MachineChecked

Lean repository linked

The Erdos discrepancy problem

Terence Tao · 2015

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.

Report this listing