AI and Mathematics Research Watch

Research updatesSelect an entry to read more

15 Oct 2026 · 16:54 CEST2 entries · 6 linked sources Partial coverage

First Proof's third batch reports nine successful proofs out of ten, with exposition and attribution still lagging Mohammed Abouzaid, Nikhil Srivastava, Rachel Ward and Lauren Williams Published: 14 Oct 20263 sources

First Proof tested five systems on ten research problems with previously unpublished human solutions of at most twelve pages. According to its results announcement, ProofCouncil answered nine correctly and the direct GPT-6 Astra test seven; the Kimi K3-based entrant answered none correctly. Expert reviewers graded anonymized submissions separately for correctness, exposition and attribution. The organizers report that only four direct-model solutions had adequate citations, compared with seven for ProofCouncil. Testing occurred on 2–5 October and expert grading on 8–9 October; 14 October is the results publication date.

Research relevance:

This provides a more relevant assessment for research mathematicians than contest scores: naturally arising research statements, expert scrutiny, separate communication criteria, and linked artifacts. Reported costs of $1,888 for ProofCouncil and $36 for the direct model also expose the practical tradeoff between orchestration, computation and success.

Claim status:: Published benchmark findings with expert review reported by the independent evaluation project. The report landing page and official announcement were read. This is evidence about performance on selected, already human-solved problems, not an announcement of ten newly solved open problems.
Limitations:: Only ten selected problems were tested. The individual referee reports, proofs and logs were not read, and the linked GitHub directories failed to load. No formal verification was established here. Comparisons with earlier batches involve different problems, and one open-weight entrant cannot establish a universal open-versus-closed capability gap.

Sources & further reading

Link to this entry

Bloom announces a shorter exposition of the AI-generated Egyptian-fraction argument Thomas Bloom and Wouter van Doorn Published: date not established3 sources

In the supplied API thread dated 14 October, the account attributed to Thomas Bloom announces a fifteen-page exposition with Wouter van Doorn of an Egyptian-fraction manuscript from the earlier OpenAI release. The thread says their exposition proves that every a/b with 0 < a < b is a sum of O(log log b) distinct unit fractions. It also reports that the original manuscript contains both a complicated route and a shorter route to the relevant bound; the exposition adopts the latter. This is a new exposition and scrutiny lead concerning an older release, rather than a fresh discovery claim.

Research relevance:

If confirmed from the paper, the update offers a tractable number-theory case study in turning AI output into readable mathematics and identifying redundant proof machinery. The thread points to a combination of sum-product theory and weak Goldbach as ingredients worth examining.

Claim status:: Author-attributed announcement in supplied API posts, with a linked proof exposition. The mathematical statement and simplification are reported claims; the PDF was not retrieved. Bloom's official website corroborates his research identity and connection to Erdős Problems, but the exact social handle was not independently authenticated.
Limitations:: The exposition's original publication date is unknown, so published_date is null; 2026-10-14 dates the announcement. The thread explicitly says the authors had not read all details of the more complicated route. The PDF failed to load, preventing assessment of hypotheses, attribution and proof details. No peer review, independent verification or checked formalization is established here.

Sources & further reading

Link to this entry

Coverage and limitations

Research window: 2026-10-13 08:25:48 to 2026-10-15 16:54:47, Europe/Paris. Public web search was used. Publication dates, supplied API post dates and search indexing dates were treated separately.
Directly read First Proof's official website, third-batch page and press release, its Hexagon report landing page, Terence Tao's blog, Thomas Bloom's official website and research page, Kevin Buzzard's Xena blog, and Simon Frieder's blog index. First Proof's linked GitHub referee-report and submission directories failed to load; individual solutions and reports were not inspected.
Bloom's official website identifies him as a Manchester mathematician and links Erdős Problems, corroborating the scholarly context. An official-site link authenticating @thomasfbloom was not found. Buzzard's Imperial webpage corroborates Xena's identity. Other supplied social handles were not independently authenticated and are not treated as certified identities.
Supplied X collections reported ok for __alpoge__, scottnarmstrong, littmath, alexkontorovich, boazbaraktcs, leanprover, axiommathai and epochairesearch, with posts supplied. Collections reported ok with no posts for wtgowers, sebastienbubeck, f_charton, leonard41111588, projectnumina and harmonicmath. These were bounded collections excluding replies and reposts, potentially including cached posts; they do not constitute fresh, complete timeline reads. No numerical X collection budget or skipped-account list was supplied.
The supplied thomasfbloom X collection was partial: pagination or a post cap was reached, leaving the timeline incomplete. Its supplied API thread was read as source material. Fetching the original X announcement through the web tool failed, and the linked UnitFractions.pdf failed repeatedly. Neither an indexed snippet nor the supplied thread substitutes for reading that paper.
The xenaproject.bsky.social collection reported ok with no posts; replies and reposts were excluded and at most 300 posts were checked. The Mathstodon collection, identified in the supplied data as mathstodon.xyz, was unavailable because of an HTTPError, with the same exclusions and 300-post cap. Neither empty results nor failed collection establishes absence of news.
Xena's latest displayed post was dated 1 October; Frieder's displayed blog entries were from 2025 or earlier. These were not presented as new. The already-covered Lean 4.35 release was not repeated merely because its social announcement appeared on 13 October. The Dialectical Theorem was submitted on 9 October despite its 14 October social circulation and was omitted as older commentary.
Additional searches consulted indexed leads including Papers With Lean and AI Proved What. These did not establish further eligible results. OpenAI's history page did not expose usable revision text in the retrieved view. Coverage of the supplied accounts and related primary sources remains incomplete. No source code was executed, no proof was verified, and Lean was not run.

Requested coverage window: 2026-10-13T08:25:48.118690+02:00 — 2026-10-15T16:54:47.359674+02:00.

Public web research; coverage is not exhaustive. A source link is not a certification of a claim.

Archives 55

Older editions (25)