Daily field radar

AI4Math Radar

Start with A Machine-Checked Proof that Gardam's $\tilde{A}_2$ Lattice Does Not Have Unique Products, then An exponential lower bound for the bit pigeonhole principle in resolution over parities. 16 fresh useful item(s) are inside the 21-day content window.

2026-09-22
Latest Newer Older
America/Los_Angeles Generated 2026-09-22T15:47:43Z JSON data
2core
14adjacent
74downweighted
0warnings

Today's Scan

Start with A Machine-Checked Proof that Gardam's $\tilde{A}_2$ Lattice Does Not Have Unique Products, then An exponential lower bound for the bit pigeonhole principle in resolution over parities. 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 7.9 2026-09-17 arXiv

A Machine-Checked Proof that Gardam's $\tilde{A}_2$ Lattice Does Not Have Unique Products

Ibrahim Mian, Shayaan Siddique

Kaplansky's zero-divisor conjecture asserts that the group ring of a torsion-free group over a field has no zero divisors. It holds for every group with the unique-product property, so a counterexample can only come from a torsion-free group without unique...

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 search loop: proposal source, verifier call, retry strategy, and stopping rule.

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

AI math reasoningLean proof agentsverifier feedback
Open PDF Semantic Scholar
2
core score 6.5 2026-09-19 arXiv

An exponential lower bound for the bit pigeonhole principle in resolution over parities

Kamil Braun

Resolution over parities, $\mathrm{Res}(\oplus)$, is the characteristic-two version of resolution over linear equations: clauses are disjunctions of affine equations over $\mathbb F_2$. Superpolynomial size lower bounds were previously known only for restri...

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 Read if you have 5 minutes and want a direct AI4Math signal.

Lean proof agents
Open PDF Semantic Scholar
3
adjacent score 4.9 2026-09-21 arXiv

Counterexamples to Grad's conjecture

Javier Gómez-Serrano, Lukas Liehr, Mitchell A. Taylor

For each sufficiently large $N$, we construct smooth solutions of the magnetohydrostatic equations on embedded solid tori whose regular pressure levels are nested tori, whose magnetic field vanishes exactly on a round magnetic axis, and whose group of Eucli...

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

Formalizing PARITY Circuit Lower Bounds in Lean

Saint Wesonga

We formalize Hastad's PARITY lower bound in Lean using the switching lemma. For every fixed d >= 2, formulas and DAG circuits of computation depth at most d computing PARITY on n inputs require size exp(Omega_d(n^(1/(d-1)))) for all sufficiently large n. Th...

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
5
adjacent score 3.5 2026-09-20 arXiv

The Positive Defect Problem: Target and Admissibility Criteria for a Programmatic Search for Unforced Navier-Stokes Blowup

Jarret Petrillo, James Glimm

On 7 and 8 September 2026 programmatic search produced singularities: a forced Navier-Stokes singularity at every fixed viscosity, statements (C) and (D) of the Clay problem, and two Euler singularities. The unforced problem, statements (A) and (B), stands...

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for 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
6
adjacent score 3.5 2026-09-20 arXiv

Distance and resistance on random series-parallel graphs: logarithmic speeds and near-critical asymptotics

Ruiqi Ding, Zehua He, Yutao Liang et al.

We study the graph distance $D_n(p)$ and effective resistance $R_n(p)$ between the boundary vertices of a depth-$n$ random series--parallel graph, obtained by recursively joining two independent copies in series with probability $p$ and in parallel with pro...

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

LIMBO: Learning and Internalizing Model-Free Barrier Objectives for Agile and Safe Whole-Body Control

Jake Gonzales, Arturo Flores Alvarez, Yu-Ming Chen et al.

Safe whole-body control requires coordinating collision avoidance and balance under high-dimensional, nonlinear dynamics--making safety certificates difficult to design and reuse across behaviors. We present LIMBO, a framework for synthesizing a state-actio...

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

verifier feedback
Open PDF Semantic Scholar
8
adjacent score 3.5 2026-09-18 arXiv

Improved bounds for universal convex covers of unit arcs

Ethan Keller

Moser's worm problem asks for a planar region of least area containing a congruent copy of every unit arc. We show that the infimum area $α$ among convex universal covers satisfies $0.239\leα\le0.24633\ldots$, reducing the gap between the previous refereed...

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

A lower bound for $\langle 3,2,m \rangle$ matrix multiplication

Askar Tsyganov, Uliana Parkina, Sergey Samsonov et al.

We prove that, over any field, the bilinear complexity of multiplying a $3\times 2$ matrix by a $2\times m$ matrix is strictly greater than $24m/5$. In particular, every exact bilinear algorithm for multiplying a $3\times 2$ matrix by a $2\times 5$ matrix r...

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

Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof

Maseeh Ghodsi

A Leech tree of order $n$ is a tree with positive integral edge weights whose $n(n-1)/2$ pairwise weighted distances are precisely $1,2,\ldots,n(n-1)/2$. This paper gives a computer-assisted proof that no Leech tree of order $18$ exists. The argument has th...

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
11
adjacent score 3.5 2026-09-17 arXiv

A Mean-Field Approach for Safe Routing of Multi-Destination Urban Air Mobility Networks

Nameer Fawwaz Ahmed, Cody Fleming, Yasser Shoukry

As Urban Air Mobility (UAM) systems scale toward high-density operations, managing autonomous Unmanned Aerial Vehicle (UAV) traffic requires control frameworks that are both tractable and safety-critical. This paper presents a principled optimal control-the...

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

The spherical cap conjecture for immersed disks

José M. Espinar

We prove that every smooth immersed disk in Euclidean three-space with nonzero constant mean curvature, regular up to the boundary and mapping its boundary diffeomorphically onto a circle, is an embedded spherical cap.

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

Watch Later

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

13
adjacent score 1.9 2026-09-21 arXiv

On the inductive blockwise Alperin weight condition for type $\mathsf B$ and type $\mathsf C$

Baoyu Zhang

The purpose of this paper is to prove that every finite simple group of type $\mathsf B$ or $\mathsf C$ satisfies the inductive blockwise Alperin weight condition at every prime $\ell$ dividing its order. For ${\rm PSp}_{2n}(q)$, where $q$ is odd and $n\geq...

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

The Taub-NUT Metric Is Not Projectively Induced

Shaosai Huang

LeBrun's Kähler realization $g_m$ of the Taub--NUT metric on $\mathbb{C}^2$ is complete, Ricci-flat and not flat. Loi, Zedda and Zuddas proved that no multiple $αg_m$ admits a Kähler immersion into a finite- or infinite-dimensional complex projective space...

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

Rogers--Ramanujan identities from the geometry of $X^a=Y^b$

Yifeng Huang, Kenny Lau, Ken Ono

We prove the conjecture of Huang, Jiang, and Oblomkov (HJO) giving a geometric extension of the Rogers--Ramanujan and Andrews--Gordon identities for every torus-knot singularity $X^a=Y^b$ with coprime $1<a<b.$ For a prime power $q$, let $\mathcal{NC}_n^{a,b...

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

A counterexample to the quantum Hedetniemi conjecture

Julius A. Zeiss

Godsil, Roberson, Šámal and Severini conjectured that the quantum chromatic number of the categorical product of two graphs equals the minimum of the quantum chromatic numbers of the factors. We disprove this conjecture: we construct explicit finite graphs...

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

leanprover/lean4: refactor: move the order-instance classification into `Sym.Arith` (#15263)

Leonardo de Moura

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

leanprover/lean4: perf: faster heuristic for LCNF's equal alt folder (#15276)

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

leanprover/lean4: fix: reuse the instances of a non-exposed definition in `inferInstanceAs` (#15216)

Attila Gáspár

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

leanprover/lean4: fix: resolve races and type errors, and prevent TCP/UDP RSS retention (#15174)

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

leanprover/lean4: fix: make the bv_decide pre-processor reduce projections and matches (#15267)

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

leanprover/lean4: fix: expose the `Char.ordinal` family (#15115)

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