By verification grade
2 of 3 carry an independent check. Open the review queue.
Open longest before falling
- 53 yrErdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateralposed 1973 · GPT-6 Astra (Codex) and Claude Opus 5.5 (Claude Code), alternating; Claude Opus 5.5 (Lean formalization)
- 46 yrErdős Problem 408: an unconditional normal order for the number of totient iterationsposed 1980 · Claude Opus 5.5 (Lean formalization); the argument is credited to Plasma AI without naming a model
- 45 yrErdős Problem 111: graphs that are not countably colorable need superlinear deletions to become bipartiteposed 1981 · GPT-6 Astra (Codex) and Claude Opus 5.5 (Claude Code), alternating; Claude Opus 5.5 (Lean formalization)
From the 3 of 3 entries recording a posed year. Add a missing one.
| Date | Finding | Lab | Model | Verification | Autonomy | Field |
|---|---|---|---|---|---|---|
| 2026-10-19 | Erdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateral | Plasma AI | GPT-6 Astra (Codex) and Claude Opus 5.5 (Claude Code), alternating; Claude Opus 5.5 (Lean formalization) | Formally verified | AI-led | mathematics |
| 2026-10-19 | Erdős Problem 111: graphs that are not countably colorable need superlinear deletions to become bipartite | Plasma AI | GPT-6 Astra (Codex) and Claude Opus 5.5 (Claude Code), alternating; Claude Opus 5.5 (Lean formalization) | Claimed | AI-led | mathematics |
| 2026-10-19 | Erdős Problem 408: an unconditional normal order for the number of totient iterations | Plasma AI | Claude Opus 5.5 (Lean formalization); the argument is credited to Plasma AI without naming a model | Formally verified | AI-assisted | mathematics |