Daily field radar

AI4Math Radar

Start with Simple symmetric Venn diagrams with 17 and 19 curves, then An exponential lower bound for the bit pigeonhole principle in resolution over parities. 15 fresh useful item(s) are inside the 21-day content window.

2026-09-23
Latest Newer Older
America/Los_Angeles Generated 2026-09-23T15:46:35Z JSON data
2core
13adjacent
75downweighted
0warnings

Today's Scan

Start with Simple symmetric Venn diagrams with 17 and 19 curves, then An exponential lower bound for the bit pigeonhole principle in resolution over parities. 15 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv14
  • 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 6.5 2026-09-22 arXiv

Simple symmetric Venn diagrams with 17 and 19 curves

Chris Dzoba

We exhibit simple, rotationally symmetric Venn diagrams with 17 curves and with 19 curves: n Jordan curves carried to one another by rotation through 2π/n, with every one of the 2^n regions present and connected and, since the diagrams are simple, every cro...

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

Hydrozoan: Latency-Adaptive DAG Consensus under Mixed Byzantine and Crash Faults

Qianyu Yu, Lefteris Kokoris-Kogias, Alberto Sonnino

DAG-based consensus protocols can achieve great throughput and the optimal three-message-delay limit for n = 3f+1 consensus. While two-delay protocols exist, they pay with reduced resilience (requiring 5f+1-style committees) or rely on fallbacks that sacrif...

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

Direct Optimization of Generators for Search in Automated Theorem Proving

Adam Ousherovitch, Ambuj Tewari

Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt generation. Recent work shows cross entropy is suboptimal for an LLM...

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

Skim cue Skim the task definition, metric, and whether the benchmark has Lean-checkable artifacts.

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

Beyond Natural Language: An Agent-Native Language for Autonomous Science

Yifeng He, Jiachen Liu

As autonomous AI agents take on every stage of scientific inquiry, research output is expanding far beyond human review capacity. Yet scientific communication still relies on natural-language prose: an informal medium prone to ambiguity, hidden assumptions,...

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

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

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

leanprover-community/mathlib4: chore(Algebra/MonoidWithZeroHom): one missed normalization to `.toMonoidWithZeroHom` (#43887)

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

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

leanprover/lean4: perf: special case single-child nodes in DiscrTree (#14805)

Robert J. Simmons

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

leanprover/lean4: fix: warn once per call of a deprecated tactic (#15286)

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

leanprover/lean4: fix: preserve sticky counts in deletion cascades (#15241)

Vincent QB, PhD

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

leanprover/lean4: chore: update Grove and address invalidated facts (#15287)

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

leanprover/lean4: chore: remove redundant instances (#9741)

Parth Shastri

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

leanprover/lean4: chore: increase priority of instSMulOfMul (#13554)

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

leanprover-community/mathlib4: refactor(RingTheory/RamificationInertia/Ramification): generalize `ramificationIdx_pos` (#41377)

Thomas Browning

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