Number theory · Sep 26, 2026
Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result
GitHub: jbaelaw/erdos1220-lean
Contributors
Claude Opus 5.5 · Claude · Codex · OpenAI · Ji Ho Bae
AI systems: Claude Opus 5.5, Claude, Codex