Convex & discrete geometry · solved
Erdős Problem 89
Solved 2 Jul 2026 by 5DAA…2rTV
- Bounty paid
- $1,194
- 5.97 τ
- Verification
- 2 min 20 s
- leanprover/lean4:v4.27.0
- Attribution
- Conjectures
Formal statement
(fun n => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)Verification report
- Manifest validpassed
- Task commitment matchespassed
- Production taskpassed
- Production sandboxpassed
- Source type hash matchespassed
- Trusted file hashes matchpassed
- Submission policy respectedpassed
- Challenge builtpassed
- Solution builtpassed
- Statement unchangedpassed
- Only permitted axiomspassed
- Lean kernel acceptedpassed
- Nanoda enablednot passed
- Nanoda acceptednot passed
Sandbox landrun+seccomp · verifier 5e92a6f7
Results are published under the Conjectures account.