proposed
reason
Candidate claim vc_cb7973c232de2315 imported from artifact packet cap_61973ee16b553d57
finding type
open_question
proposed confidence
0.99
confidence basis
agent-imported candidate claim; reviewer acceptance required
frontiers / frontier
e1271/1271 · statement.attested · reviewer:will-blair · 2026-06-10 · null→null
Reviewable change
back to reviewErdős Problem #198 has status 'disproved (lean)'. Statement: The answer is no; Erdős and Graham report this was proved by Baumgartner, presumably referring to the paper [Ba75], which does not state this exactly, but the following simple construction is implicit in [Ba75]. Let $P_1,P_2,\ldots$ be an enumeration of all countably many infinite arithmetic progressions. We choose $a_1$ to be the minimal element of $P_1\cap \mathbb{N}$, and in general choose $a_n$ to be an element of $P_n\cap \mathbb{N}$ such that $a_n>2a_{n-1}$. By construction $A=\{a_1 < a_2 < \cdots\}$ contains at least one element from every infinite arithmetic progression, and is a lacunary set, so is certainly Sidon. AlphaProof has found the following explicit construction: $A = \{ (n+1)!+n : n\geq 0\}$. This is a Sidon set, and intersects every arithmetic progression, since for any $a,d\in \mathbb{N}$, $(a+d+1)!+(a+d)\in A$, and $d$ divides $(a+d+1)!+d$. This was formalized in Lean by Alexeev using Aristotle. Topics: additive combinatorics, sidon sets, arithmetic progressions. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.
accept gate
1 of 4 on recordtimeline
vpr_65bc6ffad7c2a755Candidate claim vc_cb7973c232de2315 imported from artifact packet cap_61973ee16b553d57null→9f75542bvev_bbe9c37600e79fc2Candidate claim vc_cb7973c232de2315 imported from artifact packet cap_61973ee16b553d57proposed
reason
Candidate claim vc_cb7973c232de2315 imported from artifact packet cap_61973ee16b553d57
finding type
open_question
proposed confidence
0.99
confidence basis
agent-imported candidate claim; reviewer acceptance required
provenance
proposed by
agent:erdos-spine-ingest
actor type
agent
created at
2026-05-30
target type
finding
affected
inspect finding →Erdős Problem #198 has status 'disproved (lean)'. Statement: The answer is no; Erdős and Graham report this was proved by Baumgartner, presumably referring to the paper [Ba75], which does not state this exactly, but the following simple construction is implicit in [Ba75]. Let $P_1,P_2,\ldots$ be an enumeration of all countably many infinite arithmetic progressions. We choose $a_1$ to be the minimal element of $P_1\cap \mathbb{N}$, and in general choose $a_n$ to be an element of $P_n\cap \mathbb{N}$ such that $a_n>2a_{n-1}$. By construction $A=\{a_1 < a_2 < \cdots\}$ contains at least one element from every infinite arithmetic progression, and is a lacunary set, so is certainly Sidon. AlphaProof has found the following explicit construction: $A = \{ (n+1)!+n : n\geq 0\}$. This is a Sidon set, and intersects every arithmetic progression, since for any $a,d\in \mathbb{N}$, $(a+d+1)!+(a+d)\in A$, and $d$ divides $(a+d+1)!+d$. This was formalized in Lean by Alexeev using Aristotle. Topics: additive combinatorics, sidon sets, arithmetic progressions. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.
vf_edb314f45838fa69Read-only frontier; diff not recomputed.
Erdős problems frontier receives a reviewable source, finding, caveat, replication, evaluation, or proof-affecting edit.
The packet names affected record objects, evidence, rationale, reviewer-facing fields, and expected proof impact.
Schema, provenance, benchmark, contradiction, and proof checks decide whether the request is ready to read.
A steward accepts, rejects, caveats, revises, or retracts the request under an inspectable identity.
Only the accepted event mutates frontier state. Atlases, constellations, and search update from that record state.
Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.