proposed
reason
Manual finding added to frontier state
finding type
theoretical
proposed confidence
0.90
confidence basis
operator-supplied frontier prior; review 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 #125: machine-found Lean proof published by AlphaProof Nexus (DeepMind, arXiv 2605.22763, May 2026) (positive-lower-density variant — the formalized statement is a variant, not necessarily the full original problem). Independently re-verified locally 2026-06-10: full lake build of google-deepmind/alphaproof-nexus-results@0647711a7118 under their pinned toolchain leanprover/lean4:v4.27.0 succeeded (8062 jobs); static scan clean (no sorry, no native_decide, no custom axioms). Artifacts: erdos_125.variants.positive_lower_density.lean sha256:12e2df1ba973bde5. AI involvement: machine-generated proof, machine-checked (Lean kernel is the referee); statement faithfulness NOT yet independently attested — see paper section 4 for DeepMind's own expert validation.
- id
- vpr_ca7bf2842136ed6a
- frontier
- Erdős problems frontier
- kind
- finding.add
- created
- 2026-06-10
- findings
- +1
- state
- null → 04945ed5
accept gate
2 of 4 on record- ✓
- signature
- reviewer:will-blair · key 4892f938
- ✓
- chain
- null → 04945ed5
- —
- witness
- no verifier attachment on record for this target
- —
- grade
- in state · unreviewed
timeline
- 2026-06-10proposeproposed · finding.addagent:nexus-ingest-2026-06-10
vpr_ca7bf2842136ed6aManual finding added to frontier state - 2026-06-10acceptfinding.assertedreviewer:will-blair
null→04945ed5vev_f48dea4a3bad0f06Manual finding added to frontier state
provenance
proposed by
agent:nexus-ingest-2026-06-10
actor type
agent
created at
2026-06-10
target type
finding
affected
inspect finding →Erdős Problem #125: machine-found Lean proof published by AlphaProof Nexus (DeepMind, arXiv 2605.22763, May 2026) (positive-lower-density variant — the formalized statement is a variant, not necessarily the full original problem). Independently re-verified locally 2026-06-10: full lake build of google-deepmind/alphaproof-nexus-results@0647711a7118 under their pinned toolchain leanprover/lean4:v4.27.0 succeeded (8062 jobs); static scan clean (no sorry, no native_decide, no custom axioms). Artifacts: erdos_125.variants.positive_lower_density.lean sha256:12e2df1ba973bde5. AI involvement: machine-generated proof, machine-checked (Lean kernel is the referee); statement faithfulness NOT yet independently attested — see paper section 4 for DeepMind's own expert validation.
vf_63cf7f09150f3200Diff
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.