AI4Math

1core

15adjacent

74downweighted

0warnings

Today's Scan

Start with StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean, then A negative solution to the complemented subspace problem for Banach spaces with unconditional bases. 16 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv16

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 7.9 2026-09-08 arXiv

StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean

Idan Davidovich, Debargha Ganguly, Vikash Singh et al.

Leading benchmarks for formal theorem proving with large language models are small collections drawn from competition math, such as the IMO and Putnam, that poorly represent field-specific applications. We introduce StochBench, a Lean 4 benchmark of 450 gra...

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.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-09-08 arXiv

A negative solution to the complemented subspace problem for Banach spaces with unconditional bases

Antonio Acuaviva

We give a negative solution to the complemented subspace problem for Banach spaces with unconditional bases over both the real and complex fields. For every $ρ>0$, we construct a projection $P_ρ$ of norm less than $1+ρ$ on a separable superreflexive space \...

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.7 2026-09-06 arXiv

A Solution to Iima--Yoshino Problem 2.3

Junyu Guo, Hao Shen, Junqi Liu et al.

Iima and Yoshino asked for an ideal $I$ in $S=k[x_1,x_2,\ldots]$, with $\operatorname{deg} x_i=i$, and a monomial order such that $S/I\cong k[x_i:i\equiv\pm1\pmod5], \operatorname{in}(I)=(x_i^2,x_ix_{i+1}:i\geq1).$ We construct such an ideal and monomial or...

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 for later unless the title matches your current proof-agent work.

Lean proof agentsseed author: Junqi Liu

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 3.5 2026-09-09 arXiv

Private communication via zero-private-capacity quantum channels

Chengkai Zhu, Xin Wang

Private communication over a noisy quantum channel requires reliable transmission to the receiver and secrecy from the environment. Whether two channels with zero private capacity can jointly enable private communication is a longstanding open problem in qu...

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-09 arXiv

Finite presentations of metabelian groups: effective enumeration via Laurent relations

Achyuth Jayadevan

For an ordinary finite presentation $P=\langle x_1,\ldots,x_n\mid R\rangle$, put $G(P)=F_n/\langle\langle R\rangle\rangle$. We construct a primitive-recursive predicate $V$ with $G(P)''=1 \Longleftrightarrow \exists c\in\mathbb{N}: V(P,c)=1$. Thus finite pr...

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-09 arXiv

A Dimension-Independent Commutator Bound

Hao Shen, Jiaqi Wang, Lihong Zhi

We prove that every trace-zero matrix $A\in M_n(\mathbb{C})$ admits a representation $A=BC-CB$ with $B,C\in M_n(\mathbb{C})$ and $\lVert B\rVert\lVert C\rVert\le K\lVert A\rVert$, where $K$ is an absolute constant independent of $n$, and $\lVert\cdot\rVert$...

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 for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-08 arXiv

Second derivatives of $p$-adic $L$-functions and the Shafarevich--Tate group of rank-two CM elliptic curves

Barinder S. Banwait

For an elliptic curve $E/\mathbb{Q}$ of rank two with complex multiplication, Coates, Liang and Sujatha gave a criterion for the vanishing of $Sha(E/\mathbb{Q})[p^\infty]$ at a good ordinary prime $p$ and applied it to five such curves for $p < 30{,}000$. W...

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-08 arXiv

Nonexistence of a Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof

Kay Akiyama

We prove that no strongly regular graph with parameters $(266, 45, 0, 9)$ exists. The proof is formalized in Lean 4 and Mathlib without external infeasibility certificates or assumed classification theorems. A hypothetical graph gives a rank-$12$ integral G...

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 for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-08 arXiv

Generalized DBLog: A Verified Contract for Interleaving Database Rows with a Change Log

Andreas Andreakis

Change-data capture (CDC) feeds downstream systems like caches, search indexes, and data warehouses from a database's log of committed row changes. When bootstrapping, adding a table, or repairing downstream data, a pipeline must also copy existing rows. Me...

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-08 arXiv

Counting Survivor Sets: Exponential Equivalence with Prime-Admissible Sets

Mario Raso, Daniele Venturi

For each integer $n\geq 1$, let $N(n)$ denote the number of distinct subsets of $\{2,\ldots,n+1\}$ obtained by choosing one forbidden residue class modulo each integer from $2$ to $n$; this is OEIS sequence A396595 (https://oeis.org/A396595). Equivalently,...

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 for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-07 arXiv

Maximal Hamiltonicity of realization graphs of degree sequences

Jeffrey S. Baggett

We prove that the realization graph of every graphical degree sequence is maximally Hamiltonian: it is Hamilton-laceable when bipartite on more than one vertex, and Hamilton-connected otherwise. This answers Problem P59 of Mütze's survey of combinatorial Gr...

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-07 arXiv

Classification of Conformally Covariant 2-Tensors from the Kulkarni--Nomizu Product in Dimension 4

Yury N. Berdinsky

We classify all natural, conformally covariant, symmetric (0,2)-tensors of conformal weight -2 and differential order less than or equal to 4 in dimension 4, built from the metric, the Schouten tensor, covariant derivatives, and the Kulkarni-Nomizu product....

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 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 3.5 2026-09-07 arXiv

A construction of F-irregular graphs

James Alexander Schreib

For a fixed graph F, the F-degree of a vertex v in a host graph H is the number of subgraphs of H isomorphic to F that contain v, and H is F-irregular if its F-degrees are pairwise distinct. We show that every finite connected graph F on at least three vert...

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-06 arXiv

A dot-product bound from separate growth-minimizing bases

Zhipeng Lu

For every finite $P\subset\mathbb{R}^2$ we prove $|\{p\cdot q: p,q\in P\}|\gg |P|^{199/295}$, with an absolute constant and no logarithmic loss, where $199/295 = 2/3+7/885$. This improves the bound $2/3+7/1425$ of Kokkinos (arXiv:2502.12727), which in turn...

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-05 arXiv

Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt

Yupeng Ren, Zhaoxuan Li, Rui Zhang

Large language models (LLMs) have recently made substantial progress in formal proof generation, yet presenting distinctive challenges in cryptographic area. Computational security arguments posit that a valid proof must coordinate probability, adversarial...

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

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.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 1.9 2026-09-07 arXiv

A Proof of Bala's Congruence Conjectures for A158690

Ahaan Kallat

Let $a(n)$ be the sequence A158690 in the On-Line Encyclopedia of Integer Sequences (OEIS), defined by the exponential generating function $\sum_{n\ge0} a(n)t^n/n! = 1+\sum_{m\ge1}\prod_{j=1}^m(1-e^{-(2j-1)t})$. We prove two congruence conjectures of Peter...

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

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.

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 74 low-priority match(es), folded for daily reading.

negative score 0.8 2026-09-10 GitHub

leanprover/lean4: fix: use CMAKE_COMMAND instead of bare cmake in build (#15001)

Joe Hendrix

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-10 GitHub

leanprover/lean4: fix: update to mimalloc 3.4.5 (#15060)

Sebastian Ullrich

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-10 GitHub

leanprover/lean4: fix: restore trailing whitespace of nested tactic blocks in the info tree (#15093)

Sebastian Ullrich

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-10 GitHub

leanprover/lean4: fix: expose Vector DecidableEq for kernel reduction (#14988)

Kim Morrison

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-10 GitHub

leanprover/lean4: fix: expose Array.zipWith for kernel reduction (#15078)

Kim Morrison

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-10 GitHub

leanprover/lean4: fix: expose Array.ofFn for kernel reduction (#14989)

Kim Morrison

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-10 GitHub

leanprover/lean4: fix: expose Array.modify for kernel reduction (#15079)

Kim Morrison

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-10 GitHub

leanprover/lean4: fix: expose Array.mapM for kernel reduction (#14996)

Kim Morrison

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