Daily field radar

AI4Math Radar

Start with AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics, 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.

2026-09-09
Latest Newer Older
America/Los_Angeles Generated 2026-09-09T18:48:44Z JSON data
1core
15adjacent
74downweighted
0warnings

Today's Scan

Start with AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics, 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.

1
core score 9.5 2026-09-04 arXiv

AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics

Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund et al.

Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring th...

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

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.

autoformalizationLean proof agentsmathlib search
Open PDF Semantic Scholar
2
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
3
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.

4
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
5
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
6
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
7
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
8
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
9
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
10
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
11
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
12
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

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

A global spectral gap for Metropolis-adjusted Langevin algorithm with a uniformly randomized step size

Qian Qin

Let $π(\mathrm{d} x)\propto e^{-U(x)}\,\mathrm{d} x$ on $\mathbb R^d$, where $0<m\leq L<\infty$, $mI_d\preceq\nabla^2U(x)\preceq LI_d$, and $κ=L/m$. It is known that, under warm-start assumptions, fixed-step Metropolis-adjusted Langevin algorithm (MALA) wit...

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

Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications

Jiaming Zhao, Bing Wu, Xu Miao

Finite model finders cannot witness an Austin law: an identity whose finite models are all trivial but which has a nontrivial infinite model. We introduce rank-decreasing sparse trace-tree magmas, finitely presented total operations on a countably infinite...

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
15
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
16
adjacent score 1.9 2026-09-04 arXiv

Purely Periodic Three-move Subtraction Games

Hikaru Manabe

A subtraction game is played on a heap of tokens. The players take turns removing s tokens for some s in a fixed set S of positive integers, and the player who cannot move loses. The sequence of Sprague-Grundy values of such a game is eventually periodic. W...

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

leanprover/lean4: fix: show goal of empty nested `by` block at positions indented past the enclosing tactic (#15095)

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

leanprover/lean4: fix: floatLetIn should be pessimistic in the presence of side effects (#15089)

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

leanprover/lean4: feat: sandbox `lake challenge` with `bwrap` instead of `landrun` (#15005)

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

leanprover/lean4: feat: missing order instances for `Fin` (#15092)

Julia Markus Himmel

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

leanprover/lean4: feat: linearity marker for HashMaps (#15049)

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

leanprover/lean4: chore: stop creating lean-pr-testing-* branches in reference manual (#15074)

Garmelon

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

leanprover/lean4: chore: fixup riscv-ast bench (#15084)

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