Development

An Erdős problem falls and holds across 180,000 lines of formal proof

development2026-06-28

Claim

Erdős problem #870 fell to GPT-5.5-Pro, then held up across 180,000 sorry-free lines of Lean 4, a scale of formalization no one had attempted before.

Reported metric: 180,000 lines of Lean

Reporting date: 2026-06-28 (not necessarily the event date)

Sources

Attribution and reporting linked by this record; links do not imply independent verification.

Welcome to June 28, 2026 (theinnermostloop.substack.com)

Knowledge graphopen in browser →

Reported in

Welcome to June 28, 2026

Actor

OpenAI

Evidence for

Supersedes

A leading physicist credits a model with generalizing a calculation

Referenced by

Cite or correct this record

Citation formatCitation text

An Erdős problem falls and holds across 180,000 lines of formal proof
Innermost Loop KB — secondary record
Reporting date: 2026-06-28
KB permalink: https://nicholsn.github.io/innermost-loop-kb/developments/2026-06-28-an-erdos-problem-formalized-at-unprecedented-scale
Claim: Erdős problem #870 fell to GPT-5.5-Pro, then held up across 180,000 sorry-free lines of Lean 4, a scale of formalization no one had attempted before.
Attributed sources:
- Welcome to June 28, 2026 — https://theinnermostloop.substack.com/p/welcome-to-june-28-2026
This citation does not imply independent verification of linked-source claims.

Suggest a correction — opens a GitHub draft for you to review and submit.