Mixed campaignmathematics · formal mathematics
AlphaProof Nexus searches open Erdős and OEIS problems
A Lean-guided campaign reported nine Erdős results and 44 OEIS conjecture proofs, while also documenting failure modes such as restating the hard step behind a new unproved lemma.
Editorial context
What happened
The campaign illustrates why formal verification, statement fidelity, novelty, and mathematical significance must remain distinct fields.
Keep in view
Results for stronger or related variants must not be counted as literal resolutions of the canonical problems; full per-run transcripts are unavailable.
Chronology
Timeline
Formal-proof-search paper postedpreprint · day date
Trust boundaries
Validation
Lean checks the formal statements; experts reportedly audited correspondence to the intended problems.
System
AI and tools
- AlphaProof Nexus
- Gemini prover and rater agents
- Lean
People
Human contributors
- George Tsoukalas
- AlphaProof Nexus collaborators
Organizations
Affiliations
- Google DeepMind
Primary materials