AI4Math

3core

17adjacent

69downweighted

0warnings

Today's Scan

Start with Autoformalizing Argumentative Material Inferences, then Long-horizon autoformalization of a core theorem underlying MIP* = RE. 20 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv19
GitHub1

Best Use

Open only the first lane during a busy morning. Older recurring seeds are kept below the daily scan instead of competing with fresh items.

Start Here

The top few items most likely to matter for formal proof agents or Lean-facing AI4Math work.

core score 9.5 2026-09-15 arXiv

Autoformalizing Argumentative Material Inferences

Xin Quan, Reto Gubelmann, André Freitas

Natural language arguments are compelling before they are formally explicit. A premise supports a claim through defeasible warrants, background commitments, and exception conditions that the text leaves implicit. However, formal verification requires the op...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Read if you have 5 minutes and want a direct AI4Math signal.

autoformalizationverifier feedback

Open PDF Semantic Scholar

core score 6.5 2026-09-17 arXiv

Long-horizon autoformalization of a core theorem underlying MIP* = RE

Sirui Lu, Ruixuan Deng, Yanqiao Zhu et al.

Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Dr...

Why it matters Useful for the informal-to-formal bottleneck: it is about preserving mathematical intent across the translation boundary.

Skim cue Skim the search loop: proposal source, verifier call, retry strategy, and stopping rule.

Read if Read if you have 5 minutes and want a direct AI4Math signal.

autoformalizationLean proof agents

Open PDF Semantic Scholar

core score 6.5 2026-09-16 arXiv

FloatLib: Verified Floating-Point Arithmetic in Lean

Robert Joseph George, Will Adkisson, Anima Anandkumar

We present FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean 4 that combines broad format coverage, machine-checked correctness, and efficient certified execution. To our knowledge, FloatLib is the first Lean library to unif...

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for agents.

Skim cue Skim the task definition, metric, and whether the benchmark has Lean-checkable artifacts.

Read if Read if you have 5 minutes and want a direct AI4Math signal.

Lean proof agentsmathlib search

Open PDF Semantic Scholar

Worth Opening

Good candidates after the first three. These are plausible paper-tab opens, not a mandatory reading list.

adjacent score 4.9 2026-09-16 arXiv

Beyond Sendov's conjecture: the quadratic Tang--Zhang inequality

Teng Zhang

Very recently, Lech Mazur proved the celebrated Sendov conjecture, and Terence Tao subsequently distilled the main ideas of the proof in a blog post. In this paper, we establish a quantitative strengthening of Sendov's conjecture, namely the quadratic Tang-...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-09-15 arXiv

Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194

Cameron Beeley

For a finite simple graph G, let alpha(G) denote its independence number and let l_avg(G) = (1 / |V(G)|) sum_{v in V(G)} alpha(G[N_G(v)]) be the average independence number of its open neighbourhoods. Written on the Wall II Conjecture 194 asserts that every...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-17 arXiv

Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof

Maseeh Ghodsi

A Leech tree of order $n$ is a tree with positive integral edge weights whose $n(n-1)/2$ pairwise weighted distances are precisely $1,2,\ldots,n(n-1)/2$. This paper gives a computer-assisted proof that no Leech tree of order $18$ exists. The argument has th...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim the search loop: proposal source, verifier call, retry strategy, and stopping rule.

Read if Save for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-17 arXiv

LLVM Translation Validation Automated with Large Language Models and Lean

Chunhao Liao, Hongxu Xu, Xintong Zhou et al.

LLVM is the cornerstone of modern compilers, but its subtle intermediate representation (IR) semantics make transformations error-prone and necessitate formal verification. Alive2, a state-of-the-art translation validator based on satisfiability modulo theo...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim the abstract first; open the paper only if the method touches proof agents or formal verification.

Read if Save for later unless the title matches your current proof-agent work.

verifier feedback

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-16 arXiv

Descriptive Complexity in Lean: Completeness by First-Order Reductions

Pierre Senellart, Anton Gnatenko

We show that descriptive complexity can serve as a foundation for formalizing computational complexity results in a proof assistant, by constructing a Lean library centered around the following concepts: decision problems are isomorphism-invariant predicate...

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save if you are thinking about retrieval, premise selection, or library search.

mathlib search

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-16 arXiv

A Strongly Aperiodic Monotile in Three Dimensions

Ioannis Tsiokos

Socolar and Taylor asked for a single, simply connected three-dimensional prototile that forces nonperiodicity by shape alone, admitting no weakly nonperiodic tiling; the Schmitt-Conway-Danzer biprism and the three-dimensional Socolar-Taylor tile admit scre...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-15 arXiv

Palindromic Length in Free Groups: Reflections, Noncrossing Matchings, and Catalan Forms

Junjie Liao

Let $F=F(X)$ be a free group of finite rank, with palindromic length taken with respect to the fixed basis $X$. We embed $F$ as the index-two subgroup of the universal Coxeter group $W=F\rtimes_θ\langle t\mid t^2=1\rangle$, where $θ(x)=x^{-1}$ for $x\in X$,...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-15 arXiv

On complemented subspaces of $L_1[0,1]$

Antonio Acuaviva

We construct two complemented subspaces of $L_1[0,1]$. The first has the Schur property but fails the Radon--Nikodým property. The second contains a copy of $\ell_2$ but no copy of $L_1[0,1]$. Neither space is isomorphic to a Banach lattice. This gives a ne...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-15 arXiv

Formalization of Landau damping in the Vlasov--Poisson equations in Lean

Jacob Bedrossian

We present a formalization in Lean 4 of Mouhot and Villani's theorem on nonlinear Landau damping in $\mathbb T^d$ in all Gevrey regularity indices $s > 1/3$ for small backgrounds.

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

Watch Later

Adjacent formalization or infrastructure signals. Keep them in peripheral vision unless they match an active project.

adjacent score 2.0 2026-09-16 GitHub

leanprover-community/mathlib4: fix(Algebra/MonoidWithZeroHom): normalize to `.toMonoidWithZeroHom` (#43728)

Jiedong Jiang

Recent commit on leanprover-community/mathlib4.

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for agents.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

seed author: Jiedong Jiang

Open Semantic Scholar

adjacent score 1.9 2026-09-17 arXiv

Rogers--Ramanujan identities from the geometry of $X^a=Y^b$

Yifeng Huang, Kenny Lau, Ken Ono

We prove the conjecture of Huang, Jiang, and Oblomkov (HJO) giving a geometric extension of the Rogers--Ramanujan and Andrews--Gordon identities for every torus-knot singularity $X^a=Y^b$ with coprime $1<a<b.$ For a prime power $q$, let $\mathcal{NC}_n^{a,b...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoning

Open PDF Semantic Scholar

adjacent score 1.9 2026-09-17 arXiv

Paths maximize the expected range of graph-indexed random walks

Yinfeng Zhu

We prove that a path maximizes the expected range of a uniformly chosen graph homomorphism into the integers, with one vertex pinned at zero, among all connected bipartite graphs of the same order. This establishes the expectation form of the Benjamini--Häg...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoning

Open PDF Semantic Scholar

adjacent score 1.9 2026-09-17 arXiv

A counterexample to the quantum Hedetniemi conjecture

Julius A. Zeiss

Godsil, Roberson, Šámal and Severini conjectured that the quantum chromatic number of the categorical product of two graphs equals the minimum of the quantum chromatic numbers of the factors. We disprove this conjecture: we construct explicit finite graphs...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoning

Open PDF Semantic Scholar

adjacent score 1.9 2026-09-16 arXiv

On a conjecture of Browning and Sawin on random hypersurfaces with sign coefficients

Ken Ono, Ashvin Swaminathan

Browning and Sawin conjectured that random hypersurfaces with sign coefficients are smooth with probability tending to one as the degree grows. We prove this conjecture and obtain a quantitative bound. For each $n\geq1$, a degree $d$ form in $n+1$ variables...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoning

Open PDF Semantic Scholar

adjacent score 1.9 2026-09-16 arXiv

A Walk From Free Probability to Matrix Discrepancy II: Weaver's Problem and the Kadison-Singer Conjecture

Tarun Kathuria

\cite{mss2015} proved Weaver's discrepancy result existentially, resolving the Kadison--Singer conjecture . Finding such signs efficiently for general inputs remained an open algorithmic question. In the real-arithmetic model, we give a deterministic algori...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoning

Open PDF Semantic Scholar

Older but Useful

0 relevant item(s) are outside the 21-day content window. Keep them for context, but do not let them drive today's scan.

No older useful items were retained in this run.

Downweighted 69 low-priority match(es), folded for daily reading.

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: refactor: rename WP.wpTrans to WP.trans and the wp_consequence family to wp_monotone (#15171)

Sebastian Graf

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: refactor: delete docstring extension bootstrap helpers (#15213)

David Thrane Christiansen

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: feat: rewrite the Verso docstring parser to produce accurate syntax (#15064)

David Thrane Christiansen

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: feat: lake: separate `leanir` job (#14906)

Mac Malone

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: chore: upgrade to LLVM 23.1.1 (#15212)

Henrik Böving

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: chore: update stage0

Lean stage0 autoupdater

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: chore: bootstrapping for Verso parser rewrite (#15211)

David Thrane Christiansen

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-09-18 GitHub

leanprover/lean4: chore: block some more tests in fsanitize (#15214)

Henrik Böving

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

Source Health

Warnings are preserved so failed sources do not silently disappear from the brief.

None