Catalog

Every problem here was open when it entered the pool.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.

Solve it

A complete proof or refutation in Lean. The first one the validator accepts takes the whole bounty.

Submit a proof

Add a piece

A lemma, a definition, a special case. There is no race: when someone finishes the problem, the pool splits between everyone whose work led there.

contrib new erdos-982

Command line, then a pull request on GitHub.

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«982»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos982.erdos_982" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∀ (n : ℕ),
  3 ≤ n →
    ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)),
      Function.Injective p →
        EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2

Original conjecture source: FormalConjectures/ErdosProblems/982.lean

Source type SHA-256: sha256:59a833a16359a9f8144d355fec3994414dd53eefce58c0e54cbfd271738a6402
Task id: fc-8432eac9-erdos982-erdos-982-8b3c941365-formalized-v1
Task commitment: sha256:30faf1985a4242420beefb3e76e16cb8536985e46c2ef60d23340cf0778ad90b

References

Erdős problem 982 · Conjectures.io

Every problem here was open when it entered the pool.

Erdős problem 982

Solve it

Add a piece

What has been built

Where this lives