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 · 4 linked sources Partial coverage
A block-based “Integer Game” extends the experimental Visual Lean interface Alex Kontorovich (announcement; handle-to-person association not independently verified) Published: 4 sources

A directly collected X post announces a second experiment with the block-based Lean interface previously demonstrated through the Natural Number Game, provisionally titled “The Integer Game,” and links to a video demonstration. This is a genuine update to the earlier Visual Lean item, but presently an interface experiment rather than a new mathematical result or released formal development.

Research relevance:

A visual, block-oriented layer could lower the entry barrier to Lean and provide a practical way to teach integer reasoning while retaining a connection to formal proof syntax. If released with actual Lean checking, it could also serve as a lightweight prototype for more accessible formalization workflows.

Claim status:
Announcement only. The X API directly supplied the dated post. Alex Kontorovich’s official Rutgers page confirms his mathematical and Lean-related roles, but does not independently authenticate the X handle. The linked demonstration could not be read, and no claim of an available proof, independent scrutiny, released code, or checked Lean formalization is made.
Limitations:
The announcement gives no public source-code or application link, technical specification, licensing information, theorem coverage, or evidence that generated blocks elaborate or compile in Lean. The YouTube page was unavailable to the web reader. This may be a prototype or mock-up; its relationship to the separately indexed Visual Lean project is not established beyond the wording of the post.

Sources & further reading

Link to this entry
Coverage and limitations
  • Time window checked: 2026-10-18T21:47:43+02:00 through 2026-10-20T08:00:01+02:00. Earlier material was excluded unless needed for context, and supplied previous items were not repeated.
  • Direct X API collection was available but bounded for @__alpoge__, @scottnarmstrong, @wtgowers, @SebastienBubeck, @thomasfbloom, @littmath, @AlexKontorovich, @f_charton, @Leonard41111588, @boazbaraktcs, @leanprover, @ProjectNumina, @HarmonicMath, @axiommathai, and @EpochAIResearch. Replies and reposts were excluded; cached posts could be included; pagination was incomplete and no numerical post cap was supplied. API account resolution is not independent identity verification. All feeds were empty in the window except @AlexKontorovich, @boazbaraktcs, and @HarmonicMath. The latter two contained no substantive mathematical research update.
  • The supplied @AlexKontorovich post was read directly from the collected X API data, not merely from an indexed snippet. Rutgers’ official mathematics website confirms Alex Kontorovich’s professional identity and involvement with the Lean Focused Research Organization, but it does not independently bind that X handle to him; attribution therefore remains qualified.
  • Kevin Buzzard’s Bluesky feed @xenaproject.bsky.social was collected successfully but returned no posts. Collection excluded replies and reposts and checked at most 300 posts; an empty result does not establish inactivity.
  • Terence Tao’s Mathstodon feed could not be collected because of an HTTP error. Replies and reposts would have been excluded and at most 300 posts checked. No claim of direct Mathstodon coverage is made.
  • Terence Tao’s official What’s New yearly archive, Kevin Buzzard’s Xena blog index, Simon Frieder’s official blog, Scott Armstrong’s research website, Thomas Bloom’s website, and Alex Kontorovich’s Rutgers page were directly consulted. The accessible indexes showed no additional substantive in-window update beyond the social lead reported below.
  • Public web searches also covered recent Lean, autoformalization, AI-for-mathematics papers, repositories, and related announcements. Some search results were indexed snippets rather than directly read sources; none supplied a sufficiently substantiated additional in-window item.
  • The linked YouTube page for the Integer Game demonstration could not be fetched by the web tool, so its video contents, uploader identity, and behavior were not independently inspected. No source code, live application, Lean artifact, or kernel-check report was found. Public-web coverage is not exhaustive, particularly for unindexed repositories and incomplete social timelines.

Requested coverage window: 2026-10-18T21:47:43.225596+02:00 — 2026-10-20T08:00:01.807955+02:00.

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

Archives 55
Older editions (25)