AI & Maths watch GitHub

Retrospective research digest

Updates on artificial intelligence for mathematical research, proof discovery and formal verification, with links to papers, code and tools.

At a glance1 entry · 5 linked sources Partial coverage

One substantive September 20 assessment was established: scrutiny of the attribution and verification behind an AI-assisted social-choice result. No new theorem or completed formalization was securely dated to this day. Archival coverage remains incomplete.

Research updatesSelect an entry to read more

September 20 scrutiny separates an AI-assisted voting theorem from benchmark verification Vlad Makarov, Traictory Published: 5 sources

Traictory examines Epoch AI's classification of the approval-based committee-election core problem as a human-plus-AI solution. The underlying Becker–Greger–Peters preprint was submitted on September 10, not September 20: it claims that a core committee always exists, using a harmonic-entropy objective, and gives polynomial-time computation. The September 20 contribution is scrutiny of the evidence: Epoch's original task requested an empty-core counterexample, so its instance checker cannot certify the authors' universal existence proof. Epoch attributes the primary idea and proof to a lengthy interactive session with GPT-6 Astra and says a simple prompt does not appear sufficient.

Research relevance:

Relevant to social choice, combinatorial optimization and research evaluation. It illustrates why computationally checkable constructions, universal proofs and attribution of mathematical ideas require different evidence.

Claim status:
Dated secondary assessment, supported by an available primary preprint and Epoch's attribution statement. The authors explicitly credit GPT-6 Astra. The assessment is scrutiny of benchmarking and provenance, not an independent mathematical verification of the proof.
Limitations:
Older result assessed on September 20. No peer-review outcome or Lean formalization was established from the consulted sources. Epoch's current pages corroborate the account but do not independently establish when the classification first appeared. The article provides a publication date without a timestamp or timezone. I did not verify the proof or run its algorithm.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed September 20, 2026, for the Paris civil-day window. Publication dates were distinguished from underlying result dates and search-index dates. Sources displaying only a calendar date did not establish a precise publication time or timezone.
  • Read the dated Traictory assessment, Epoch AI's committee-election page and benchmark FAQ, and the underlying arXiv paper's abstract, publication history and selected HTML passages. Epoch's current pages were consulted retrospectively; their exact September 20 contents were not independently archived.
  • Consulted Terence Tao's September archive, Gowers's Weblog, Xena, Leonardo de Moura's blog index and Axiom's blog index. Kevin Buzzard's Imperial webpage explicitly identifies https://xenaproject.wordpress.com/ as his blog. Older entries, including previously supplied September 18 material, were excluded.
  • Checked personal or organizational websites for Alpöge, Armstrong, Bloom, Litt, de Moura, Barak, Lean, Harmonic, Axiom and Epoch. These checks did not authenticate every supplied social handle. Armstrong's and Barak's websites link to social accounts, but opening those links failed. The attempted Bubeck, Charton and Kontorovich homepage addresses failed to load; Project Numina's homepage returned no readable text.
  • Date-specific searches covering all supplied X handles produced no usable September 20 posts. Additional searches for Tao's Mathstodon and Buzzard's Bluesky accounts established no eligible posts. Indexed profile and mirror snippets were leads only; no exhaustive social-platform access or complete account history was available.
  • Read Reservoir's GroupApproximation description, which mentions September 20 integration and Lean progress. Both linked dated reports failed to load, and the mutable description did not establish their original publication dates. These leads were excluded, together with undated announcements and material published on other days.
  • Read Daniel Lemire's September 20 commentary but omitted it because it offers broad institutional predictions without a concrete mathematical result or research tool. A World Programming Society lead failed to load. Other daily-digest snippets were used only for discovery; their edition dates were not treated as dates of underlying news. No source code was executed and no Lean proof was checked.

Requested coverage window: 2026-09-20T00:00:00+02:00 — 2026-09-21T00:00:00+02:00.

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

Archives 32
Older editions (2)