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 glance2 entries · 5 linked sources Partial coverage

Two dated contributions were established for October 5, 2026: an exposition of the Lyons–White result with a qualified AI formalization claim, and a proposal for evaluating research amid AI-driven publication growth. Social-media archival coverage remains incomplete.

Research updatesSelect an entry to read more

Axiom explains the Lyons–White exponent dichotomy and its qualified Lean formalization Colin Defant Published: 4 sources

Defant’s new exposition explains an older result with Ken Ono: for symmetric continuous-time random walks on dihedral groups, increasing jump rates cannot increase distance from uniform at positive even exponents. For every finite non-even exponent p ≥ 1, some dihedral group admits a counterexample. The positive result extends to inversion extensions of finite abelian groups. The article connects the distinction to Fourier analysis and the Hardy–Littlewood majorant phenomenon, and links the paper and Lean repository.

Research relevance:

A concrete connection between probability, harmonic analysis and AI-assisted formalization, with public mathematical arguments and formal artifacts available for scrutiny.

Claim status:
October 5 exposition of an available August 27 preprint, not a newly published proof. The authors report AxiomProver formal verification assuming standard literature. The repository README reports local comparator verification; this digest did not reproduce it or establish independent scrutiny.
Limitations:
The paper includes p = 1 in its counterexample statement, while the repository README advertises counterexamples for p > 1. Their scopes should therefore not be equated without inspecting the formal statements. The literature assumptions and correspondence between informal and formal results require auditing. The broader index-two abelian-subgroup extension remains a conjecture in the exposition.

Sources & further reading

Link to this entry
Pasquato proposes limiting publication-based evaluation to protect research quality Mario Pasquato Published: 1 source

Pasquato argues that AI makes paper production a weaker signal of scientific achievement. He proposes restricting annual publication output, or the papers considered by funding and hiring committees, while allowing AI assistance under human responsibility. The October 5 essay updates an earlier May piece to address developments in mathematics and explicitly acknowledges that mathematical authorship conventions and publication rates require different implementation choices.

Research relevance:

Relevant to mathematicians serving as editors, referees or evaluators: it offers a concrete institutional response to increased AI-generated submissions and incentives that reward volume over intelligibility.

Claim status:
A dated policy proposal and argument, not an adopted rule or empirical demonstration. The page records receipt on September 3 and revision on October 1; public publication is dated October 5.
Limitations:
Much of the argument originates in astrophysics and an older May essay. The proposed two-paper annual threshold has no demonstrated effectiveness here. October 5 comments raise concerns about early-career opportunities, predatory journals and the difficulty of reviewing longer consolidated papers.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed October 5, 2026, the Paris civil day. Original publication dates were distinguished from submission, revision and indexing dates; sources without publication times retain boundary uncertainty.
  • Read Axiom’s dated article, the underlying arXiv abstract and HTML paper, and the linked GitHub repository README. The mathematical preprint was submitted August 27, 2026; October 5 marks the new exposition, not a new theorem.
  • Read Proofs and Prompts and Mario Pasquato’s October 5 contribution, including its stated relationship to an older May essay.
  • Consulted Terence Tao’s blog, Xena, Lean’s official website, Epoch AI’s website, Harmonic’s website, Thomas Bloom’s website and Daniel Litt’s official website. Kevin Buzzard’s Imperial webpage explicitly links to https://xenaproject.wordpress.com/, establishing the official Xena address. These checks did not authenticate every supplied social-media handle.
  • Date-specific searches used the supplied names and organizational leads. Indexed X profiles and third-party mirrors provided incomplete, often relative-dated material; they did not establish usable October 5 posts. No exhaustive access to X, Mathstodon or Bluesky was obtained. The supplied accounts remain leads where official linkage was not established.
  • Project Numina’s website returned no readable text. Jonathan Leake’s blog appeared in an indexed snippet dated October 5, but direct retrieval failed; its contribution was excluded. A attempted Leonardo de Moura website retrieval also failed.
  • Excluded older papers resurfaced in the October 5 AI4Math Radar, event pages whose event or modification dates did not establish original publication dates, sponsored prize publicity, and later OpenAI-release discussion. October 5 dates embedded in repository filenames alone were insufficient evidence of public release that day.
  • No source code was executed, no Lean build was run, and no proof was independently verified. Absence of accessible dated posts does not establish absence of other news.

Requested coverage window: 2026-10-05T00:00:00+02:00 — 2026-10-06T00:00:00+02:00.

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

Archives 36
Older editions (6)