Let $F$ be a family of sets closed under taking subsets (i.e. if $B \subseteq A \in F$ then $B \in F$ ). There exists some element $x$ such that whenever $F^{'} \subseteq F$ is an intersecting subfamily we have $∣ F^{'} ∣ \leq ∣{A \in F : x \in A}∣ .$

Worked, still open.

combinatorics · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Write (\mathcal F_x:={A\in\mathcal F:x\in A}) [[nomath]](the “star” at $x$)[[/nomath]]. Your statement says:

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 · open (literature)

theorem erdos_701 : answer(sorry) ↔ ∀ {X : Type} [Nonempty X] [Fintype X],
    ∀ (F : Set (Set X)), IsLowerSet F →
      ∃ x : X, ∀ᵉ (F' ⊆ F),
        F'.Intersecting →
          (#F' ≤ #{ A : Set X | A ∈ F ∧ x ∈ A })

formal-conjectures/701.lean ↗

status

open

evidence

formal

status

Search Vela