Vela

Let be an infinite cardinal and be the successor cardinal of . Can one colour the countable subsets of using many colours so that every with contains subsets of all possible colours?

Worked, still open.

set theory · 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

Let (\mu:=2^{\aleph_0}) and (\kappa:=\mu^+). The question is asking for a coloring [ c:[m]^{\aleph_0}\to \kappa ] such that for every (X\subseteq m) with (|X|=\kappa), [ c\bigl[[X]^{\aleph_0}\bigr]=\kappa, ] i.e. every (\kappa)-sized $X$ is “fully polychromatic” on its countable subsets [[nomath]](in partition notation…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 3 5 · open (literature)

theorem erdos_598 : answer(sorry) ↔
    ∃ c : { s : Set m // s.Countable } → κ.out,
    ∀ X : Set m, #X = κ →
    c '' { s : { sub : Set m // sub.Countable } | s.1 ⊆ X } = Set.univ
formal-conjectures/598.lean ↗

status

open

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 8822adbd09e591428e9b4f97f24ff6e573edfc541530df6a9aed4ed04bbf4414

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.