qedbot

Erdős·erdos:501

Erdős Problem 501

conjecture formal record: mixed source: not disprovable 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

1 Jun 2026·with Sungchul Lee

Candidate conditional partial result (conditional solution to first part)

candidate A1 V0 F2
Reasoning and sources

Autonomy

AI collaborating with humans

Claimed on erdosproblems.com

1

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

Fidelity

How fidelity is graded

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

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

As each project's formalization.yaml states 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.

Something wrong or missing here? Request a correction or add a claim, with its sources.

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

Cite this record

qed.bot, “Erdős Problem 501”, https://qed.bot/s/erdos-501, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.