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 glance5 entries · 10 linked sources Partial coverage

Five substantive entries were identified for September 26, 2026: an AI-assisted polytope preprint, two dated Lean registry records, a reproducibility package for a nested recurrence, and an essay on research values. Archival social-media coverage remains incomplete.

Research updatesSelect an entry to read more

AI-assisted preprint gives counterexamples and bounds for cube-truncated Hadamard simplices Nikita Lebedev Published: 2 sources

The preprint claims a nonintegral example in dimension eleven and proves that smaller dimensions cannot supply one, characterizes smoothness, and establishes normality for every smooth member of the specified family. It also presents an integral but nonnormal example in dimension fifteen and sharp uniform integrality bounds for Sylvester simplices. The author discloses generative AI assistance with proof exploration, verification code and editing.

Research relevance:

Concrete progress on lattice-polytope questions, accompanied by ancillary Lean sources, verification scripts and a map between paper statements and formal results.

Claim status:
An available research manuscript. The author reports Lean counterparts of all 17 numbered results, using standard Lean axioms. This digest read the manuscript's formalization description but did not check the proofs or run Lean.
Limitations:
Normality is established in specified parameter regions; the remaining parameters are not completely classified. Formal coverage concerns numbered statements, not prose or priority claims. Independent scrutiny was not established. The arXiv submission timestamp is September 26 at 21:20:49 UTC, within the Paris target day; it does not separately establish the public announcement time.

Sources & further reading

Link to this entry
Dated Lean registry record claims Hamilton cycles in Cayley graphs of polylogarithmic degree Shengtong Zhang, formalization maintainer Published: 3 sources

Palomar registered a formalization claiming that, for absolute constants C and n0, every connected Cayley graph on n at least n0 vertices with degree at least C(log n)^13/log log n has a Hamilton cycle. The dated record concerns a proposed theorem from an underlying September 25 research draft. Current repository documentation describes AI-assisted manuscript preparation and an agent-generated Lean development.

Research relevance:

If the mathematical and formal statements withstand scrutiny, the result substantially lowers the degree threshold for Hamiltonicity in arbitrary connected Cayley graphs and provides reusable spectral, matching, rounding and absorption infrastructure.

Claim status:
The public registry feed records publication on September 26 at 03:17:12 UTC. Its abstract claims complete formalization with only standard Lean axioms. Current repository documentation reports kernel and Comparator checks, while explicitly stating that no human has reviewed the Lean statement or proof and that the manuscript has not been refereed.
Limitations:
This is a degree-restricted Cayley-graph result, not a solution of the full Lovász conjecture. The underlying manuscript describes a proposed proof without independent verification. The immutable source snapshot could not be opened; current README explanations are retrospective clarification whose revision date was not established. No proof was verified for this digest.

Sources & further reading

Link to this entry
Erdős Problem #1220 receives a dated Lean record for non-provability in ZFC Ji Ho Bae (JRTI) Published: 3 sources

Palomar registered a Lean development expressing the affirmative answer to Erdős Problem #1220 as a first-order sentence and proving its non-provability in ZFC. The question concerns a partition relation at a singular cardinal under countable-power inaccessibility assumptions. Repository documentation attributes the underlying negative consistency result to Shelah and Stanley's 1987 forcing construction.

Research relevance:

A substantial formalization of forcing and partition calculus, with separate targets for non-provability and correspondence between the logical sentence and the mathematical problem.

Claim status:
The readable registry feed records publication on September 26 at 02:04:54 UTC. An indexed registry excerpt reports successful Comparator, Lean-kernel and NanoDa checks, plus automated statement review. The full entry rendered only a JavaScript shell. Repository documentation was read; neither its proof nor its build was independently checked.
Limitations:
The formalization establishes the recorded non-provability claim; it does not formalize consistency of the affirmative answer or full independence. The mathematical result is older material newly formalized and registered, not a newly solved conjecture. Automated review is not human peer review or a novelty certificate.

Sources & further reading

Link to this entry
Padovan recurrence reproducibility package archives finite-state computations and Lean proofs Benoit Cloitre, Haobo Ma and Wenlin Zhang Published: 2 sources

A Zenodo release archives computations, Lean proofs and verification records for identifying OEIS A076502 through Padovan numeration. The package covers discrepancy bounds, an explicit morphic presentation and a claimed least balance constant of four. Its accompanying arXiv paper was submitted September 27 and is a later explanatory source, not a September 26 publication.

Research relevance:

A reproducible computer-assisted approach to a nested integer recurrence, connecting automata, numeration systems, symbolic dynamics and formal proofs.

Claim status:
The original Zenodo record explicitly dates version v1.0.1 to September 26 and lists a downloadable archive. The package description reports formal proofs and verification records. The later preprint explains the mathematical claims; this digest did not inspect the archive or validate its certificates.
Limitations:
The GitHub repository and tagged release could not be fetched. AI involvement was not established from the accessible package description. Zenodo supplies a publication date without a time-zone-resolved timestamp, so exact placement within the Paris civil day cannot be independently reconstructed.

Sources & further reading

Link to this entry
Ivan Corwin proposes evaluating AI use through the broader value of mathematical research Ivan Corwin Published: 1 source

Corwin argues that mathematical value extends beyond resolving posed problems to developing understanding, training students, sustaining research communities and serving society. He sees potential for AI to connect ideas across fields, while warning that offloading intellectual work can weaken the learning and shared understanding needed for future research.

Research relevance:

A framework for deciding which AI-assisted activities merit research effort and recognition, especially when theorem production becomes easier than explanation and training.

Claim status:
A dated original guest essay on Terence Tao's blog. It presents judgments about mathematical practice, not a new theorem, empirical evaluation or formalization.
Limitations:
The essay offers a normative framework rather than a tested workflow. Its examples of AI-enabled mathematical advances are contextual claims, not independently verified results in this digest. Later comments were not treated as September 26 evidence.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed the Paris civil day September 26, 2026. Original source dates and registry publication timestamps were used; search crawling and indexing dates were not treated as publication dates.
  • Read arXiv metadata and the HTML manuscript for Lebedev's Hadamard-simplex paper, the dated Zenodo Padovan package record, Palomar's public JSON feed, relevant GitHub documentation, and Ivan Corwin's original guest post on Terence Tao's blog.
  • Consulted Tao's September archive and Mastodon links, Kevin Buzzard's Imperial webpage and Xena blog, Daniel Litt's blog, Boaz Barak's Windows On Theory blog, François Charton's website, and official Lean, Axiom, Epoch AI and Harmonic websites. Numina's website returned no readable text; Armstrong's blog timed out.
  • Checked supplied identity leads against personal or institutional websites where accessible. Armstrong and Barak's websites link their social accounts; Buzzard's Imperial webpage confirms https://xenaproject.wordpress.com/ as his blog. Several supplied handles could not be independently confirmed. No item relies on an unconfirmed social-media identity.
  • Date-specific searches across the supplied X handles returned no usable original September 26 posts. Indexed profiles and mirrors do not provide exhaustive historical access. Tao's Mathstodon profile returned minimal text, and Buzzard's supplied Bluesky profile could not be fetched.
  • Palomar entry pages returned JavaScript shells. Their public JSON feed was readable, and an indexed excerpt supplied additional verification details for Erdős Problem #1220. Individual immutable JSON records and the pinned Lovász GitHub snapshot could not be fetched; current repository documentation is identified as retrospective clarification.
  • Excluded previously supplied entries and sources dated outside the target day. The Padovan arXiv preprint was submitted September 27; only its September 26 software package is included. Additional registry leads were not promoted into entries where version history or proof scope remained insufficiently examined.
  • No source code was executed, no Lean build was run, and no mathematical proof was independently verified.

Requested coverage window: 2026-09-26T00:00:00+02:00 — 2026-09-27T00: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)