Erdős problem 701

Let

\mathcal{F}

be a family of sets closed under taking subsets (i.e. if

B\subseteq A\in\mathcal{F}

then

B\in \mathcal{F}

). There exists some element

x

such that whenever

\mathcal{F}'\subseteq \mathcal{F}

is an intersecting subfamily we have

\lvert \mathcal{F}'\rvert \leq \lvert \{ A\in \mathcal{F} : x\in A\}\rvert.

Withdrawn 6 Oct 2026

SOLVED_EXTERNALLY (the release coordinator confirmed that arXiv:2609.19123v1 and arXiv:2609.28404v2, Theorem 1, settle the finite hereditary-family case, which is the pinned target over finite ground types, with a public Lean formalization. This retirement did not independently rebuild that proof. See EXTERNAL-SOLUTIONS-2026-10-06.md.)

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«701»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos701.erdos_701" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ {X : Type} [Nonempty X] [Fintype X] (F : Set (Set X)),
    IsLowerSet F → ∃ x, ∀ F' ⊆ F, F'.Intersecting → Cardinal.mk ↑F' ≤ Cardinal.mk ↑{A | A ∈ F ∧ x ∈ A}

Original conjecture source: FormalConjectures/ErdosProblems/701.lean

Task id: fc-6a786f99-erdos701-erdos-701-5af5e2048d-formalized-v1
Task commitment: sha256:23babed48cd514be93812602fa03c3142c76b04f038faa1f1112a2d0cef3523c

References

erdosproblems.com/701

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord