AWESOME AI PROOFS
← Problems
Research / Sep 3, 2026

Erdős–Sós tree-embedding conjecture, benchmark formulation (Erdős

Does every sufficiently edge-dense graph contain every tree of the prescribed size?

Model / AI: GPT-6 Astra

machine-checked (formal benchmark statement)self-reported (formal benchmark statement)
Sep 3, 2026

Autonomous Lean proof of the benchmark statement

Model / AI: GPT-6 Astra

machine-checked (formal benchmark statement)self-reported (formal benchmark statement)

A pre-release GPT-6 Astra run in Epoch AI's LeanOpenProblems harness produced a Lean proof using a permutation-word counting argument. The repository reports no human steering and a Comparator check against the benchmark statement.

Source read 2026-09-08. Read the repository's scope and verification account. The build was not rerun and the statement was not audited against every classical formulation.