Daily field radar

AI4Math Radar

Start with Autoformalizing Argumentative Material Inferences, then Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization. 17 fresh useful item(s) are inside the 21-day content window.

2026-09-17
Latest Newer Older
America/Los_Angeles Generated 2026-09-17T19:12:17Z JSON data
2core
15adjacent
73downweighted
0warnings

Today's Scan

Start with Autoformalizing Argumentative Material Inferences, then Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization. 17 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv16
  • 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.

1
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
2
core score 6.5 2026-09-13 arXiv

Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization

Andre Panossian

Scientific autoformalization turns verbal accounts into executable mathematics, but executable code does not settle which model has been constructed. We examine two sources of structural uncertainty: the formalizer that generates a response law, and the rec...

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
3
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

Worth Opening

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

4
adjacent score 4.9 2026-09-13 arXiv

The Colomo-Pronko conjecture for frozen-corner alternating sign matrices

Yinjie Li

We prove the Colomo-Pronko conjecture for alternating sign matrices with a prescribed square of zeros at a corner, for all matrix sizes and freezing parameters. A known multiple-integral formula for the frozen-corner count yields determinant representations...

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
5
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
6
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
7
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
8
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
9
adjacent score 3.5 2026-09-15 arXiv

Certified Inference and Training for Deep Equilibrium Networks: A Continuation Framework with Polynomial Complexity Guarantees

Alex Borisevich

We develop a certified continuation framework for equilibrium computation and for training deep equilibrium networks (DEQs), with training formulated as interpolation to accuracy $2^{-b}$. For inference, compact input homotopy selects a unique branch from a...

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

Protected tails and polynomial-time enumeration of permutations avoiding a direct sum of an increasing pattern and 231

Henning Ulfarsson

We give an exact algorithm counting the permutations that avoid a fixed pattern from the following family: the direct sum of an increasing pattern and the pattern 231. The first members of the family are 1342 and 12453. For each member, the algorithm comput...

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

Fast Stencil Computations on a Single Arbitrarily Moving Interval

Aaron Gregory

A stencil computation repeatedly updates every cell of a grid from its neighbours' values at the previous timestep. Simulating T steps on N cells directly costs Theta(NT), and a line of work beginning with Ahmad et al. reduces this by composing many timeste...

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

A Lean Paper About Paper: A Formal Framework for Origami

Celio Boulay, Alexander Chai, Anthony Chang et al.

The mathematics of Origami have been well studied and shown to develop several interesting results. We use Lean 4 tactics and build on Mathlib to redefine the 7 Huzita operations as theorems instead of axioms and prove their existence. We develop proofs for...

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

A Walk From Free Probability to Matrix Discrepancy I: Matrix Spencer

Tarun Kathuria

The Matrix Spencer conjecture asks whether any $n$ real symmetric matrices A_1,...,A_n \in \mathbb{R}^{m \times m} of operator norm at most one admit a signing $x\in\{-1,1\}^n$ such that the operator norm of the signed sum is at most O(\sqrt{n \log(2m/n)})...

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
17
adjacent score 1.9 2026-09-14 arXiv

Optimal entanglement-assisted source coding under a balanced-difference promise

Julius A. Zeiss

Entanglement can reduce the communication required for coding tasks, but establishing the minimum achievable cost is essential to understanding its limits. We address this question in a zero-error source-coding task where Alice receives a word and Bob knows...

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

leanprover/lean4: perf: parse `erased` doElem quotations with the compiled grammar (#15199)

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

leanprover/lean4: feat: lake: `copy` option for path dependencies (#15142)

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

leanprover/lean4: feat: add `lake samply` command (#12545)

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

leanprover/lean4: doc: update Grove, add table for order API adoption in numeric types (#15120)

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

leanprover/lean4: chore: update release scripts (#15187)

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

leanprover-community/mathlib4: feat(Tactic): general tactic to translate `(E)NNReal`, `ENat`, `PNat` goals to `Real` and `Nat` (#43254)

Vasilii Nesterov

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.

Open Semantic Scholar

Source Health

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

  • None