AI & Maths watch GitHub

Archived edition

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

Research updatesSelect an entry to read more

3 entries · 10 linked sources Partial coverage
Tao proposes an AI-assisted challenge to extract explicit tenth-discriminant bounds Terence Tao Published: 3 sources

Tao proposes a Polymath-style experiment: use disclosed AI assistance to extract and optimize effective upper bounds for a hypothetical tenth Heegner discriminant from several recent arguments excluding Landau–Siegel zeros. The task is deliberately applied to a class-number problem already solved by other methods, reducing the danger of disrupting an active priority race. Tao suggests that sufficiently effective and clean bounds could yield another proof of the class-number-one result and perhaps a high-quality Lean formalization suitable for Mathlib.

Research relevance:

This is a concrete research workflow rather than a benchmark: compare different proofs by forcing their constants to become explicit, retain scientifically useful negative results, publish large artifacts in repositories, disclose AI use, and optimize for human-verifiable arguments rather than speed. It is a plausible model for using AI on tedious quantitative bookkeeping while leaving mathematical interpretation and quality control visible.

Claim status:
Open research challenge, not a result. Tao has specified a task and evaluation criteria, but the post itself supplies no new tenth-discriminant bound, no new proof of the class-number-one theorem, and no Lean formalization.
Limitations:
Formal verification is optional in the challenge. Tao suggests independent AI checking for purely AI-generated submissions, which is weaker than expert review or formal verification. Any future bound will still require scrutiny of hypotheses, constants, and its correspondence with the cited source argument.

Sources & further reading

Link to this entry
Tao publishes a human-oriented sketch of the AI-generated Landau–Siegel-zero argument Terence Tao Published: 4 sources

Tao gives a compact exposition of Ben Green’s five-page reformulation of an OpenAI-generated argument excluding Landau–Siegel zeros. The route bounds the weighted number of primes for which a quadratic character is negative and then invokes standard analytic number theory to exclude exceptional zeros. Tao places Green’s version alongside independent digestions by William Banks and Bryce Kerr and discloses using the SAIR open math model while studying the preprints. Relative to the previously reported Green manuscript, the update is a separate expert exposition connecting the key estimate to the classical analytic consequences.

Research relevance:

For researchers assessing AI-produced mathematics, this supplies a useful layer between a model-generated manuscript and full verification: an established number theorist isolates the main estimate, relates it to parity-breaking phenomena, compares alternative human rewrites, and records where an AI assistant entered the reading process.

Claim status:
Available expert exposition of an earlier claimed result, with multiple human rewrites cited. This is meaningful scrutiny and digestion, but it is not a peer-review verdict, an independent line-by-line verification, or a formalization. Banks’s earlier manuscript supplies explicit constants and states that the underlying ideas come from the OpenAI manuscript; Green supplies a shorter variant rewritten by him after an AI-assisted session.
Limitations:
The blog post is dated 2026-10-19 but provides no publication time, so it may fall just before the window’s 20:00 CEST boundary. Tao omits portions described as standard analytic number theory. No Lean artifact is linked for this argument, and this digest did not verify the proofs. The wider quasi-Riemann-hypothesis manuscripts are described as still being digested.

Sources & further reading

Link to this entry
Readable Intelligence releases paper maps and readable versions for AI-generated mathematics Readable Intelligence Published: 6 sources

Readable Intelligence presents an independent prototype for navigating OpenAI’s large collection of AI-generated mathematics. Its reader combines original papers with rewritten versions, dependency maps of definitions and results, notation support, passage-level questions linked back to sources, and comments. At inspection time it listed 722 source papers but only six papers with readable versions. The instructions used to generate readable versions and paper blueprints are publicly available for inspection and contribution.

Research relevance:

The dependency map directly addresses a practical problem raised by very long model-generated proofs: locating which lemmas support a result before attempting detailed checking. Publishing the rewriting and mapping instructions also makes the transformation workflow inspectable and potentially adaptable to other mathematical collections.

Claim status:
A publicly accessible prototype and open-source workflow were directly observed. Thomas Bloom’s supplied X post dated 2026-10-20 recommended the paper-map feature after trying it, but this is limited user feedback, not an accuracy evaluation. The project explicitly says it is independent of OpenAI and is not an official review of the underlying papers.
Limitations:
The project page itself gives no launch date; 2026-10-20 is the date of the supplied public announcement lead, not a dated release record on the site. Only six readable versions were available, institutional email is required for interactive participation, and neither rewrites nor dependency maps certify mathematical correctness. The project says its current rewriting method is experimental. This digest did not test the assistant, validate a map against a full paper, or execute repository code.

Sources & further reading

Link to this entry
Coverage and limitations
  • Time window: 2026-10-19 20:00 CEST to 2026-10-21 08:00 CEST. Terence Tao’s posts expose calendar dates but not publication times; the 2026-10-19 item may predate the window’s 20:00 start and is explicitly treated as time-uncertain.
  • Directly read public sources included Terence Tao’s official What’s New blog, Readable Intelligence’s website and methodology pages, its public source repository, OpenAI’s public mathematics repository, arXiv metadata, Ben Green’s manuscript, the Xena blog, and Simon Frieder’s official blog. Search results and indexed snippets were used only for discovery, not as proof of claims.
  • X API collection reported status ok for @__alpoge__, @scottnarmstrong, @wtgowers, @sebastienbubeck, @thomasfbloom, @littmath, @alexkontorovich, @f_charton, @leonard41111588, @boazbaraktcs, @leanprover, @projectnumina, @harmonicmath, @axiommathai, and @epochairesearch. The supplied collection was bounded, may contain cached posts, excluded replies and reposts, and supplied no numeric pagination or budget limit. Empty feeds do not establish inactivity. API account resolution is not independent identity verification.
  • The supplied X posts were read directly through the provided API data, not through complete X timelines. Thomas Bloom’s 2026-10-20 posts supplied the lead for Readable Intelligence; the tool and its features were then checked against the project’s own public pages and repository. Other supplied X posts were repeats, commentary, event promotion, or insufficiently substantive for inclusion.
  • Bluesky collection for @xenaproject.bsky.social reported status ok but returned no posts; replies and reposts were excluded and at most 300 posts were checked. This does not establish that no posts appeared.
  • Mathstodon collection for Terence Tao failed with an HTTP error. Replies and reposts were excluded and at most 300 posts would have been checked. Tao’s official blog was available, but his Mathstodon timeline was not.
  • The Xena and Simon Frieder blogs showed no qualifying new post in the reporting window. Public web search cannot guarantee exhaustive discovery, and direct timelines beyond the supplied API results were not claimed. No source code or Lean development was executed.

Requested coverage window: 2026-10-19T20:00:01.807955+02:00 — 2026-10-21T08:00:02.062739+02:00.

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

Archives 55
Older editions (25)