GPT-5.5 Pro solves Erdős problem #38; solution Lean-formalized

AI system

System: GPT-5.5 Pro, with Aristotle used for Lean autoformalisation
Model: Not assessed
Release: Exact release not established.
Application developer: OpenAI (GPT-5.5 Pro); Aristotle (developer not named in the cited sources)
Role: GPT-5.5 Pro generated a proof, and Aristotle converted it into Lean for verification.
Configuration: The reported configuration was GPT-5.5 Pro.
Inputs and outputs: Not assessed
Autonomy: Not assessed
Workflow: A user prompting GPT-5.5 Pro with the problem statement. Human cleanup of the written proof. Independent human check and Lean autoformalization by Aristotle. Acceptance by the site maintainer.
Human oversight: Not assessed
Relation to AI: The model produced the proof after a human prompt. Humans cleaned up the write-up and checked it, and the maintainer accepted it. A separate AI system (Aristotle) produced the Lean formalization that a human confirmed matches the paper. Tao's wiki classifies the case as AI standalone with non-significant human involvement. The attribution of GPT-5.5 Pro to OpenAI rests on the chatgpt.com share link in gebyjaff's forum post. No cited source names OpenAI in prose. The cited sources do not name Aristotle's developer.
AI contribution: The model produced the proof after a human prompt. Humans cleaned up the write-up and checked it, and the maintainer accepted it. A separate AI system (Aristotle) produced the Lean formalization that a human confirmed matches the paper. Tao's wiki classifies the case as AI standalone with non-significant human involvement. The attribution of GPT-5.5 Pro to OpenAI rests on the chatgpt.com share link in gebyjaff's forum post. No cited source names OpenAI in prose. The cited sources do not name Aristotle's developer.

Benefits

Outcome identifiers: Not assessed
Benefit: GPT-5.5 Pro solved Erdős problem #38; human-checked 26 April 2026, Lean-formalized by Aristotle 1 May, recorded as solved on erdosproblems.com
Category: Improved Knowledge Discovery
Status: Not assessed
Beneficiary groups: Organizations. Society.
Beneficiaries: Not assessed
Reach: Not assessed
Distribution and access: Not assessed
Duration: Not assessed
Expected?: Yes
Costs and harms: Not assessed

Measurement

Studies: Not assessed
Study design: Not assessed
Measurement: Not assessed
Setting and sample: Not assessed
Measures: Not assessed
Comparison: Not assessed
Results: Not assessed
Additional value from AI: Not assessed
Limitations: Not assessed
Denominators: Not assessed
Materials for replication: Not assessed

Money

Kind of value: Not assessed
Amount: Not assessed
Currency and prices: Not assessed
Period and unit: Not assessed
Realization: Not assessed
Recipients and payers: Not assessed
Gross or net: Not assessed
Included costs: Not assessed
Comparison: Not assessed
Method: Not assessed
Return and payback: Not assessed

People and places

Participants: Developer: OpenAI (GPT-5.5 Pro); Aristotle (developer not named in the cited sources). Operator: Individual user (gebyjaff) posting on erdosproblems.com.
Jurisdictions: Developer: United States.
Ownership and control: Not assessed
Dependencies: Not assessed
Cross-border connections: Not assessed
Geopolitical implications: Not assessed

Follow-up

Conditions for replication: The problem has a precise, formalized statement. The proof is checkable by humans or in Lean. A community venue reviews and records AI-produced solutions.
Replication attempts: 2 follow-up entries. Benefit recurred: 2.
Later findings: 1 May 2026. Six days after the solution was posted, the Aristotle system autoformalized the argument in Lean and a forum checker confirmed that the formalization matches the write-up; Thomas Bloom added an alternative sketch the next day, and Tao's wiki (data to 30 June 2026) lists the problem as a full AI solution.
Availability: Not assessed
Institutional decision: Not assessed
Grounds: Not assessed
Action and result: Not assessed
Success criterion: Not assessed

Evidence

Source numbers: AIBD-0075-source-0001–0003
Citations: Numbered references below.
Language: Not assessed
Source relationships: Independent
Original evidence: Not assessed
Access and versions: Not assessed
Supported findings: Not assessed
Evidence links: Not assessed
Evidence strength: Not assessed
Missing evidence: Not assessed

Grades

Assessed benefits: Organizations. Society.
Depth: Organizations: 1. Society: 1.
Reasons: Organizations: Small: one more entry resolved in the erdosproblems.com project, accepted by its maintainer. Society: Small: a single open problem settled. The problem page records the solution, and Tao's wiki catalogs it among many AI contributions.
Observed or intended: Not assessed
Rubric: Not assessed
Assessor and date: Not assessed
Alternative assessments: Not assessed
Fill: Listed, not verified

Entry details

Kind

Not assessed

Related entries

Same developer, OpenAI, and same stakeholder, the research record: the nonsense term “vegetative electron microscopy” entered published papers via AI training contamination that GPT-3 and GPT-4 reproduce, harming researchers, publishers and the scientific record.

Field

Mathematics. Research mathematics (additive number theory).

Purpose

General-purpose reasoning model prompted to solve an open research problem

Dates

Date basis unassessed: 2026 (precision unassessed). Updated: 21 October 2026.

Stage

Not assessed

Version

SHA-256: a937c036c24f…

References

Other identifiers: AI Incident Database: 1044.
Category mappings: Not assessed
Brief: Not assessed
Revisions: 6 revisions. Latest: 21 October 2026.

Sources

Other Independent author

Bloom, T. (ed.) (2026). Erdős Problem #38. erdosproblems.com.
Other Independent author

erdosproblems.com forum (2026). Thread for problem 38. erdosproblems.com.
Other Independent author

Tao, T. et al. (2026). AI contributions to Erdős problems. GitHub wiki, teorth/erdosproblems.