Erdős·erdos:949

Erdős Problem 949

conjecture formal record: mixed source: open F0 no formal statement

No formal proof attached. Any claim here rests on a write-up or a report.

Fidelity F0: Absent. No formal statement is attached to the result.

ramsey theory·Source

AI activity

AlphaProof

7 Jan 2026

Solution to variant problem (Lean)

partial A3 V2 F0

Reasoning and sources

AI standalone; human involvement recorded as non-significant

F0 no formal statement. Absent. No formal statement is attached to the result.

Follow this problem

An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.

Discussion and bounties for this problem load here.

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

Formal statements · 1

FormalConjectures/ErdosProblems/949.lean
2 declarations, 2 unproved goals·research open, research solved

Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 3

https://www.erdosproblems.com/949
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/949.lean
FormalConjectures/ErdosProblems/949.lean

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

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