proposed
reason
Candidate claim vc_dcaf7eada589de75 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
Erdős problems frontier
- id
- vfr_37aec80d874a0239
- license
- CC-BY-4.0
- findings
- 1,256
- accepted core
- 6
- contested
- 0
- links
- 17
- sources
- 1,234
- evidence
- 1,256
- avg conf
- 0.98
e1271/1271 · statement.attested · reviewer:will-blair · 2026-06-10 · null→null
Reviewable change
back to reviewadd a finding
acceptedErdős Problem #189 has status 'disproved (lean)'. Statement: If $\mathbb{R}^2$ is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area? Graham, "On Partitions of 𝔼ⁿ", Journal of Combinatorial Theory, Series A 28, 89-91 (1980). (See "Concluding Remarks" on page 96.) Solved (with answer `False`, as formalised below) in: Vjekoslav Kovač, "Coloring and density theorems for configurations of a given volume", 2023 https://arxiv.org/abs/2309.09973 In fact, Kovač's colouring is even Jordan measurable (the topological boundary of each monochromatic region is Lebesgue measurable and has measure zero). This was formalized in Lean by Alexeev and Kovac using Aristotle. Topics: geometry, ramsey theory. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.
- id
- vpr_ddf4c9af93a361f7
- frontier
- Erdős problems frontier
- kind
- finding.add
- created
- 2026-05-30
- findings
- +1
- state
- null → 7dbc09b2
accept gate
1 of 4 on record- —
- signature
- reviewer:erdos-db-trust · no key registered on this bundle
- ✓
- chain
- null → 7dbc09b2
- —
- witness
- no verifier attachment on record for this target
- —
- grade
- in state · unreviewed
timeline
- 2026-05-30proposeproposed · finding.addagent:erdos-spine-ingest
vpr_ddf4c9af93a361f7Candidate claim vc_dcaf7eada589de75 imported from artifact packet cap_61973ee16b553d57 - 2026-05-30acceptfinding.assertedreviewer:erdos-db-trust
null→7dbc09b2vev_160daa5cd32e0949Candidate claim vc_dcaf7eada589de75 imported from artifact packet cap_61973ee16b553d57
provenance
proposed by
agent:erdos-spine-ingest
actor type
agent
created at
2026-05-30
target type
finding
affected
inspect finding →Erdős Problem #189 has status 'disproved (lean)'. Statement: If $\mathbb{R}^2$ is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area? Graham, "On Partitions of 𝔼ⁿ", Journal of Combinatorial Theory, Series A 28, 89-91 (1980). (See "Concluding Remarks" on page 96.) Solved (with answer `False`, as formalised below) in: Vjekoslav Kovač, "Coloring and density theorems for configurations of a given volume", 2023 https://arxiv.org/abs/2309.09973 In fact, Kovač's colouring is even Jordan measurable (the topological boundary of each monochromatic region is Lebesgue measurable and has measure zero). This was formalized in Lean by Alexeev and Kovac using Aristotle. Topics: geometry, ramsey theory. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.
vf_b691c54cbf309acdDiff
Read-only frontier; diff not recomputed.
Review chain
- 01requestopen review →
Change request
Erdős problems frontier receives a reviewable source, finding, caveat, replication, evaluation, or proof-affecting edit.
- 02packetopen the campaign →
Diff packet
The packet names affected record objects, evidence, rationale, reviewer-facing fields, and expected proof impact.
- 03checksinspect checks →
Check output
Schema, provenance, benchmark, contradiction, and proof checks decide whether the request is ready to read.
- 04reviewread queue →
Reviewer decision
A steward accepts, rejects, caveats, revises, or retracts the request under an inspectable identity.
- 05acceptedinspect events →
Accepted event
Only the accepted event mutates frontier state. Atlases, constellations, and search update from that record state.