Daily field radar

AI4Math Radar

Start with Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization, then The Colomo-Pronko conjecture for frozen-corner alternating sign matrices. 17 fresh useful item(s) are inside the 21-day content window.

2026-09-15
Latest Newer Older
America/Los_Angeles Generated 2026-09-15T19:09:04Z JSON data
1core
16adjacent
72downweighted
0warnings

Today's Scan

Start with Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization, then The Colomo-Pronko conjecture for frozen-corner alternating sign matrices. 17 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv15
  • GitHub2

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 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
2
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
3
adjacent score 4.9 2026-09-12 arXiv

Golden-ratio growth of Conway's subprime closure

Romain Popescu

Let $s(m)$ be the Conway subprime function define the binary operation on the natural numbers $x \circ y= s(x + y)$, and denote by $C_n$, $n \ge 0$, the sequence of subsets of natural numbers defined by $C_0 = \{1\}$, and $C_{n+1} = C_n \cup (C_n \circ C_n)...

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

Lieb's Permanental Dominance Conjecture for Ordinary Immanants through Order Fifteen

Yinjie Li

Pate proved ordinary irreducible-immanant permanental dominance through order $13$ and identified $(4,4,3,3)$ as the sole remaining order-$14$ case, with $(5,4,3,3)$ and $(3^5)$ forming the order-$15$ frontier. These three cases are settled here; consequent...

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

On the Number of Distinct Topological Bases of a Finite Set of Size $N$

Lars Warren Ericson

For a finite set $S$ with $\lvert S\rvert = N$, the number of families $\mathcal{B} \subseteq \mathcal{P}(S)$ that are topological bases is $\#(N) = \sum_{\mathcal{T} \in \operatorname{Top}(S)} 2^{\lvert\mathcal{T}\rvert - \lvert\mathcal{M}_{\mathcal{T}}\rv...

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

Mechanizing Gödel's incompleteness Theorems and Provability Logic

Shogo Saitou, Mashu Noguchi

We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.

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

Gap Entropy and Almost Instance-Wise Optimal Best-Arm Identification

Jiarui Yao, Jiaxi Zhao, Xiangxin Zhou

In the best-arm identification problem, we are given $n$ stochastic arms with unknown means and wish to identify the arm with the largest mean with probability at least $1-δ$, using as few samples as possible. We consider independent Gaussian rewards with u...

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

Skim cue Skim the reward construction and whether failures provide dense learning signal.

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

Four-arm polyominoes in Golomb's hierarchy: A complete classification with Lean verification

Angel Ivanov Raychev

We classify the polyominoes obtained by adjoining four straight arms to a single square, allowing zero arm lengths, according to their ability to tile rectangles, half-strips, bent strips, quadrants, strips, half-planes, and the plane. We also classify thei...

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

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

leanprover-community/mathlib4: feat(CategoryTheory/AB5): AB5 instance of Ab with universe variables (#41737)

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 2.0 2026-09-15 GitHub

leanprover-community/mathlib4: chore(Algebra/MonoidHom): rename to `.ofClass` (#43755)

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

Greedy Packing of Nested Rings: Placement Rules, a Golden Counterexample, and a Tribonacci Floor

Javier Aguilar Martín

We study packings of annuli ("rings") of a common width into a disk, where a ring may nest inside the hole of a strictly larger one, a selection-oriented relative of the Recursive Circle Packing Problem. The two natural objectives, cardinality and contact a...

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

A Bound Below 2.8 for Tuza's Conjecture

Sichen Wang

Let $ν(G)$ be the maximum number of edge-disjoint triangles in a graph $G$ and $τ(G)$ the minimum number of edges meeting every triangle. Tuza conjectured that $τ(G)\le 2ν(G)$. We prove that $τ(G)\le (165/59)ν(G)$. The constant $165/59\approx 2.797$ improve...

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

leanprover/lean4: test: cross-check integer `@[extern]` implementations with `test_extern` (#14288)

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

leanprover/lean4: perf: share grind modifier parser construction (#15161)

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

leanprover/lean4: perf: compute library suggestion indexes on demand (#15159)

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

leanprover/lean4: fix: tcp and udp recv truncated datagram and parallel accept (#14795)

Sofia Rodrigues

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

leanprover/lean4: fix: double release when two threads stop the same libuv handle (#14793)

Sofia Rodrigues

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

leanprover/lean4: feat: frame the exception channel (#15067)

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

leanprover/lean4: feat: bundle the `con-ron` external checker (#15153)

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

Source Health

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

  • None