Daily field radar

AI4Math Radar

Start with Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification, then StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean. 20 fresh useful item(s) are inside the 21-day content window.

2026-09-14
Latest Newer Older
America/Los_Angeles Generated 2026-09-14T19:54:44Z JSON data
5core
15adjacent
68downweighted
0warnings

Today's Scan

Start with Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification, then StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean. 20 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv20

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.

1
core score 14.9 2026-09-10 arXiv

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

Joshua Ong Jun Leang, Haonan Li, Zheng Zhao et al.

Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in inf...

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 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 agentsseed author: Wenda Liverifier feedback
Open PDF Semantic Scholar
2
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
3
core score 6.5 2026-09-10 arXiv

Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Engineering

Alexander Krentsel, Shubham Agarwal, Mert Cemri et al.

Software development follows an implementation-verification loop in which developers or agents iteratively revise an implementation until an evaluator, such as a test suite, accepts it. The evaluator checks the implementation against a set of requirements u...

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 reward construction and whether failures provide dense learning signal.

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

Lean proof agentsverifier feedback
Open PDF Semantic Scholar

Worth Opening

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

4
core score 6.5 2026-09-10 arXiv

Beyond Solver Verdicts: Generative Reward Models for Autoformalization

Vikash Singh, Debargha Ganguly, Aman Goel et al.

Neurosymbolic systems rely on mathematical solvers to guarantee reasoning correctness, yet solvers are fundamentally blind to whether a formal translation maintains strict reference-equivalence to a designated formalization. We formalize this vulnerability...

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 reward construction and whether failures provide dense learning signal.

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

autoformalizationverifier feedback
Open PDF Semantic Scholar
5
core score 6.5 2026-09-10 arXiv

A Four-Valued Graph Model for Conflict Resolution: Core Framework and a Machine-Checked Formalization in Lean 4

Yukiko Kato

This note consolidates the core of the Quasi-Closed World Graph Model for Conflict Resolution (QCW-GMCR), which extends the standard Graph Model for Conflict Resolution with Belnap's four-valued logic to represent option-level epistemic ambiguity, and pairs...

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.

Lean proof agentsverifier feedback
Open PDF Semantic Scholar
6
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
7
adjacent score 3.5 2026-09-10 arXiv

Error bounds for the Sherman-Morrison formula and its modification with improved stability

Behnam Hashemi, Yuji Nakatsukasa

It is known that the Sherman--Morrison (SM) formula is not numerically stable. In recent work, we introduced SMIR, an algorithm that incorporates iterative refinement to enhance the SM backward error. In this paper we take a different route: adapting an alg...

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
8
adjacent score 3.5 2026-09-10 arXiv

A Non-constant Lower Bound for Grammar-Based Compression with Greedy

Danny Hucke

We prove a lower bound of Ω(log n/ log log n) on the approximation ratio of the global grammar-based compression algorithm Greedy. To our knowledge, the previously best lower bound was a constant, and the existence of a nonconstant lower bound had remained...

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
9
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
10
adjacent score 3.5 2026-09-09 arXiv

Henstock--Kurzweil Gauge Integral in the Non--Gaussian Regime: A Machine--Verified Construction

Yuri N. Berdinsky

We develop a machine-checked construction of non-Gaussian functional integrals using the Henstock--Kurzweil gauge integral and Chernoff product approximations. The central object is a finite family of bosonic modes with action S(phi) = (1/2) phi^T A phi + l...

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
11
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
12
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

Watch Later

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

13
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
14
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
15
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
16
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
17
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
18
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

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 68 low-priority match(es), folded for daily reading.
1
negative score 0.8 2026-09-14 GitHub

leanprover/lean4: refactor: move infotree and snapshottree utils (#15133)

Marc Huisinga

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
2
negative score 0.8 2026-09-14 GitHub

leanprover/lean4: fix: remove lossy syntax separator array coercions (#15020)

Marc Huisinga

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
4
negative score 0.8 2026-09-14 GitHub

leanprover/lean4: feat: support loading lake check and lake comparator input directly from export files (#15157)

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
6
negative score 0.8 2026-09-14 GitHub

leanprover/lean4: feat: add `--paranoid` to `lake check` and `lake comparator` (#15145)

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
7
negative score 0.8 2026-09-14 GitHub

leanprover/lean4: feat: add --inadvisably-no-sandbox to comparator (#15156)

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
8
negative score 0.8 2026-09-14 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

Source Health

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

  • None