Eight open problems from Formal Conjectures proved in Lean by a simple agent loop

A team at FAIR at Meta ran GPT-5.6 Sol in h1, a minimal loop that gives a model a Lean interface and verifier feedback, on 236 problems listed as open in Google DeepMind's Formal Conjectures repository and obtained Lean proofs of eight of them, among them a variant of Erdős Problem 337, three OEIS conjectures and the existence of an AME(9, 10) quantum state; Formal Conjectures marked five as solved.

What was found

The eight are: $W(k)/2^k \to \infty$ for two-colour van der Waerden numbers, a variant of Erdős 138; the Ruzsa-Turjányi variant of Erdős 337, that $|(A + A) \cap [1, 2N]| / |A \cap [1, N]| \to \infty$ for every asymptotic basis of density zero; the OEIS conjectures for A108081, A211417 (Bala's supercongruence, $p^{3k} \mid a(p^k) - a(p^{k-1})$ for primes $p \ge 5$) and A022030; the existence of an AME(9, 10) state, a unit vector in $(\mathbb{C}^{10})^{\otimes 9}$ whose reduction to any four parties is maximally mixed, which is Open Quantum Problem 35; and Written on the Wall II Conjectures 100 and 314. The proofs were made public on 2026-09-14 in a pull request to Formal Conjectures, merged on 2026-09-24, that marks the first five as solved with links to a repository of nine Lean files; the ninth, Green's Open Problem 25, is not counted in the paper. The paper, dated 28 October 2026, also reports that the loop exposed several misformalizations in Formal Conjectures by proving short disproofs of the written statements, including a smooth four-dimensional Poincaré variant missing a Hausdorff hypothesis.

Novelty check

The paper selected all eight from problems Formal Conjectures listed as open, and the merged pull request records the prior and concurrent work its maintainers accepted: for Erdős 138, Campos, Fox and Schildkraut's arXiv 2608.20824 of 2026-08-21, which proves $w(k) \ge (1 - o(1)) k 2^{k-1}$ with a colouring found by ChatGPT 5.6 Sol Pro and so already implies this variant, and for A211417 a 2020 proof sketch by Peter Bala on OEIS via Meštrović. arXiv, 2026-10-29: abs:"absolutely maximally entangled" AND abs:"nine" returned 4 records, none constructing AME(9, 10), and abs:"Written on the Wall" AND abs:"conjecture" returned 5, none on Conjectures 100 or 314. Within this registry 2026-05-21-alphaproof-nexus carries vibemathed's Erdős 138 record, which credits AlphaProof Nexus with an earlier result on another form of that problem; no entry covers any of these eight.

Graded formally verified for verification and search scaffold for autonomy. What these mean.

Cite this entry

whataifound.org. (2026). Eight open problems from Formal Conjectures proved in Lean by a simple agent loop. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-14-h1-formal-conjectures-open-problems

@misc{whataifound-fairatmeta-2026-problems,
  title        = {Eight open problems from Formal Conjectures proved in Lean by a simple agent loop},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by FAIR at Meta. Verification: Formally verified. Autonomy: Search scaffold.},
  url          = {https://whataifound.org/finding/2026-09-14-h1-formal-conjectures-open-problems}
}

Related findings

← All mathematics findings in the registry