qedbot

Erdős·erdos:501

Erdős Problem 501

conjecture formal record: mixed source: not disprovableno F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

A Palomar registration names this problem. It is shown below but not counted as a check of the claim.

Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

combinatorics, set theory·Source

AI activity

How grades work
GPT-5.5 Pro

2026-06-01·with Sungchul Lee

Candidate conditional partial result (conditional solution to first part)

candidate A1 collaborative V0 claimed F2 declared
Reasoning and sources

Autonomy

AI collaborating with humans

Does the formal statement say what was claimed?

F2 declared The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

declares divergences from its source reviewed by an agent

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

Checks

1
  • verified Palomar

    Registered by Palomar at 218d1c1e: Comparator confirmed 7 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

    project registered at a pinned commit·2026-09-06·commit 218d1c1e46f7

    PALOMAR-2026-08-19-000002 — names this problem; not counted as a check of the claim

Declared by the projects

1

Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict it.

Erdős Problem #501 in Lean 4: the closed case and the independence of the first questionelliotglazer/erdos501 · joined by names · Palomar

Read formalization.yaml

authors
Elliot Glazer, Sol
method
agent — Claude (Anthropic) — Fable 5 (claude-fable-5) and Opus 4.8 (claude-opus-4-8); the final integration and the Mathlib ModelTheory bridge (Erdos501/FOL/, Challenge.lean, Solution.lean) were produced by Fable 5, GPT-5.6 ("Sol")
review
agent-reviewed (Claude (Anthropic) audit sessions: statements of the seven targets against erdosproblems.com/501 and formal-conjectures (docs/audits/2026-08-16-audit-formal-conjectures-501-statements.md), the paper (docs/audits/2026-08-16-audit-rev10-profile-certificate.md), the vendored port (third_party/flypitch4/), and the forcing development (docs/audits/2026-08-17-erdos501-forcing-audit-355bc1e.txt), Elliot Glazer (review of the trusted statements and of the mathematics))
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
results
7 main results named, checked with Comparator, with an alignment table
sources
Some unsolved problems (Problem II.9) — background, authors n/a; Unsolved problems in set theory (Problem 38) — background, authors n/a; Erdős problem #501 (erdosproblems.com) — background, authors not-contacted; Erdős problem #501 — forum discussion (erdosproblems.com) — background, authors participated
related
flypitch/flypitch — builds-on; ianklatzco/flypitch — builds-on; google-deepmind/formal-conjectures — other; leanprover-community/mathlib4 — builds-on
divergences
(1) Independence is proved for the first-order sentence Erdos501 ("every complete ordered field has the Erdős property"), i.e. for the first question rendered inside ZFC; the target erdos501_sentence_faithful certifies that in Mathlib's ZFSet this sentence is equivalent to the Mathlib statement of the first question, so nothing weaker is being claimed. Inside the sentence, "outer measure < 1" is rendered as the existence of a cover by countably many open intervals of total length < 1 (the definition of Lebesgue outer measure), "bounded" as bounded above and below, "infinite" as "ω injects into X". (2) The theory ZFC is Flypitch's axiomatization (extensionality, empty set, ordered pairs, union, power set, infinity, regularity, Zorn's lemma, strong collection), which is equivalent to the usual ZFC. (3) Independence is stated semantically (Mathlib has no proof calculus): ¬ (ZFC ⊨ᵇ φ) means that some model of ZFC (with carrier in Type 0; by Löwenheim–Skolem this is no restriction) satisfies ¬φ. The underlying Flypitch results are the syntactic ¬ (ZFC ⊢ₛ' Erdos501_f) and ¬ (ZFC ⊢ₛ' ∼Erdos501_f) (comparator-flypitch.json). (4) The consistency of a positive answer is obtained from the ran
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Formal material

Formal statements · 1
Cited proofs · 2

Recorded elsewhere

Compare the registries
  • palomar — elliotglazer/erdos501

    checked·their labels: registered

  • vibemathed — Erdős Problem #501: infinite independent sets for families of small outer measure

    checked·joint·their labels: lean-verified, ai-co-developed

Also known as · 3
  • https://www.erdosproblems.com/501
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/501.lean
  • FormalConjectures/ErdosProblems/501.lean