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

1 entry · 2 linked sources Partial coverage
Harriss and Stange propose rigorous illustration as part of AI-assisted mathematical research Edmund Harriss and Katherine E. Stange Published: 2 sources

A new guest essay on Tao's blog develops a practical response to AI-generated proofs and visualization code: identify which properties an illustration supports, certify those properties mathematically, and examine how colleagues interpret the image. Algebraic starscapes illustrate how unexpected rendering behavior can suggest research questions, while early Mandelbrot images demonstrate how resolution can mislead. The essay extends discussion of their older paper, Mathematical Illustration: Proof, Intuition and AI, submitted to arXiv on October 2.

Research relevance:

Useful for researchers using AI to build exploratory graphics: the proposed workflow connects visual discovery, explicit mathematical guarantees and collaborative criticism.

Claim status:
Research-methodology essay directly read; the supporting paper's arXiv abstract and submission history were consulted. The authors report acceptance in the Notices. This is not an announcement of a newly proved theorem or checked formalization.
Limitations:
The October 11 publication time is unknown. The underlying paper and examples predate the window. The full paper was not read, its acceptance was not independently confirmed, and visualization code was not executed.

Sources & further reading

Link to this entry
Coverage and limitations
  • Window: 2026-10-11 10:01:57 to 2026-10-12 08:00:01 Europe/Paris. Publication dates were distinguished from search indexing and crawl dates. The included October 11 post has no confirmed publication time, so its placement after the window's opening time is uncertain.
  • Public web search was used. Directly consulted Terence Tao's What's New, Kevin Buzzard's Xena, Proofs and Prompts, Scott Armstrong's official website and LiebThirring repository, OpenAI's mathematics revision history, and relevant arXiv abstract and submission-history pages. No proof was verified and no Lean code was executed.
  • Identity checks: Armstrong's official website links his X account and formalization resources. Buzzard's Imperial webpage identifies Xena as his blog. Stange's and Harriss's linked websites were consulted. Independent verification of every supplied social handle was not completed; account resolution and search snippets were not treated as authentication.
  • Supplied X collection status was ok for scottnarmstrong, thomasfbloom and littmath, with posts available. Armstrong's announcement repeats the previous digest; Bloom's supplied discussion and Litt's supplied commentary did not establish a substantial new research development. Armstrong's X link failed when opened through the web tool; assessment used the supplied API material and public primary sources.
  • Supplied X collection status was ok with empty results for __alpoge__, wtgowers, sebastienbubeck, alexkontorovich, f_charton, leonard41111588, boazbaraktcs, leanprover, projectnumina, harmonicmath, axiommathai and epochairesearch. For all sixteen X feeds, collection was bounded, replies and reposts were excluded, and cached posts could be included. Numeric pagination caps, completeness, budget limits and skipped-account details were not supplied. Empty results do not establish inactivity; cached material is not a newly read timeline.
  • The supplied xenaproject.bsky.social collection was ok but empty, excluding replies and reposts and checking at most 300 posts. Its identity was not independently tied to Buzzard's official website. The supplied mathstodon.xyz collection was unavailable because of an HTTPError, with replies and reposts excluded and at most 300 posts checked; Tao's Mathstodon timeline was therefore not available.
  • Official Lean, Axiom, Harmonic and Epoch AI websites were opened. Project Numina's website returned no readable text, and Harmonic's returned very limited text. These checks did not provide exhaustive coverage of their announcements or independently authenticate every supplied handle.
  • Search-indexed X profiles and third-party social mirrors were leads only, not directly read X timelines. A secondary lead about an Etingof–Gerovitch essay could not be followed to its original publication. No item was based on that lead.
  • Excluded misleadingly fresh search hits: CAM-Bench originated in May; OpenAI's withdrawal history remained dated October 7; SqueezeBench's primary arXiv record showed October 9, despite a secondary site's October 12 update label. No in-window update was established. Previously reported Math 2.0 and Armstrong–Loher announcements were not repeated.

Requested coverage window: 2026-10-11T10:01:57.082757+02:00 — 2026-10-12T08:00:01.529738+02:00.

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

Archives 55
Older editions (25)