proposed
reason
Candidate claim vc_2e4ad5ecf784b675 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 #347 has status 'proved (lean)'. Statement: Is there a sequence $A=\{a_1\leq a_2\leq \cdots\}$ of integers with $$\lim \frac{a_{n+1}}{a_n}=2$$ such that $$P(A')= \left\{\sum_{n\in B}n : B\subseteq A'\textrm{ finite }\right\}$$ has density $1$ for every cofinite subsequence $A'$ of $A$? This has been solved in the affirmative by ebarschkis in the comments (based on idea of Tao and van Doorn, also in the comments). Thos was formalized in Lean by Barschkis using Aristotle. Topics: number theory, complete sequences. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.
- id
- vpr_bb1aedb6706a4b43
- frontier
- Erdős problems frontier
- kind
- finding.add
- created
- 2026-05-30
- findings
- +1
- state
- null → 43389d21
accept gate
1 of 4 on record- —
- signature
- reviewer:erdos-db-trust · no key registered on this bundle
- ✓
- chain
- null → 43389d21
- —
- witness
- no verifier attachment on record for this target
- —
- grade
- in state · unreviewed
timeline
- 2026-05-30proposeproposed · finding.addagent:erdos-spine-ingest
vpr_bb1aedb6706a4b43Candidate claim vc_2e4ad5ecf784b675 imported from artifact packet cap_61973ee16b553d57 - 2026-05-30acceptfinding.assertedreviewer:erdos-db-trust
null→43389d21vev_9824e3211c7c7d33Candidate claim vc_2e4ad5ecf784b675 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 #347 has status 'proved (lean)'. Statement: Is there a sequence $A=\{a_1\leq a_2\leq \cdots\}$ of integers with $$\lim \frac{a_{n+1}}{a_n}=2$$ such that $$P(A')= \left\{\sum_{n\in B}n : B\subseteq A'\textrm{ finite }\right\}$$ has density $1$ for every cofinite subsequence $A'$ of $A$? This has been solved in the affirmative by ebarschkis in the comments (based on idea of Tao and van Doorn, also in the comments). Thos was formalized in Lean by Barschkis using Aristotle. Topics: number theory, complete sequences. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.
vf_3bdeedd439e228beDiff
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.