Daily field radar

AI4Math Radar

Start with Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback, then SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization. 17 fresh useful item(s) are inside the 21-day content window.

2026-09-06
Latest Newer Older
America/Los_Angeles Generated 2026-09-06T17:39:17Z JSON data
3core
14adjacent
73downweighted
0warnings

Today's Scan

Start with Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback, then SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization. 17 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv17

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-08-31 arXiv

Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback

Gregory Morse

Classical lower bounds show that multiplying two degree-three polynomials over $\mathbb F_2$ requires nine scalar products in bilinear or quadratic models. They do not settle unrestricted Boolean multiplicative complexity: an XOR--AND circuit may reuse nonl...

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.

Lean proof agentsverifier feedback
Open PDF Semantic Scholar
2
core score 6.5 2026-08-29 arXiv

SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Hojae Han, Jongyoon Kim, Sanghyeok Park et al.

Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean. A central challenge is that current evaluation metrics can accept type-correct but misaligned statements or reject correct statements written in a diffe...

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 agents
Open PDF Semantic Scholar
3
core score 6.5 2026-08-28 arXiv

Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

Shuze Chen, Kunal Marwaha, Xiaoyang Lu et al.

Proof assistants such as Lean 4 promise the paradigm of formally verified mathematics, but large-scale formalization projects have faced major barriers to entry, including the need for expertise in formal verification (as well as the underlying mathematics)...

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.

Lean proof agentsverifier feedback
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-03 arXiv

AutoGraphForge: Towards Automated Graph Theory Discovery

Ján Pastorek

We report on our ongoing project to develop a computational pipeline, AutoGraphForge, for an automated graph-theoretic conjecturing-refuting-formalizing-proving system. Conjecture generation is counterexample-guided and runs in rounds: a Graffiti3 generator...

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.

AI math reasoningLean proof agents
Open PDF Semantic Scholar
5
adjacent score 4.9 2026-08-30 arXiv

The S-matrix conjecture

Yinjie Li

Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix $A\in\mathbb R^{n\times n}$ satisfies $\|A^{-1}\|_F\ge 2n(n+1)^{-1}\|A\|_{\max}^{-1}$, with equality precisely for positive multiples of $S$-matrices. Cheng proved the conject...

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
6
adjacent score 4.9 2026-08-30 arXiv

Separating Parsing Expression Grammars using Cell-Probe Lower Bounds

Jungyeom Kim, Jihyeok Park

We resolve three open problems concerning parsing expression grammars (PEGs). We construct a single language $C$ satisfying $C\in\mathsf{LIN}\cap\mathsf{PEG}$ and $C^R\in\mathsf{LIN}\setminus\mathsf{PEG}$. This proves that some linear context-free language...

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
7
adjacent score 4.9 2026-08-29 arXiv

Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free

Maher Kallel, Mohamed El Louadi

In May 2026 an OpenAI model produced a counterexample to the Erdős unit distance conjecture. Five mathematicians published a human-verified version the same day, and the result entered the literature within weeks. In August 2026 the same laboratory publishe...

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

SparseStack Is an Optimal Oblivious Subspace Embedding

Diar Heidary

The fully independent SparseStack sketch is a vertical stack of $s$ independent CountSketch matrices, scaled by $s^{-1/2}$, so that every column has exactly $s$ nonzero entries. We prove that it is an oblivious subspace embedding for $d$-dimensional subspac...

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-08-31 arXiv

Colombo's Determinant Problem

Qianli Ma

We completely solve Colombo's 1928 determinant problem. For distinct real $x_1,\ldots,x_N$, $N\geq 2$, and an integer $D\geq 1$, we prove that $\det[(x_j-x_i)^D]\neq 0$ if and only if $D\geq N-1$ and either $N$ is even or $D$ is even. The even-exponent case...

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-08-28 arXiv

Fine Difference Structure and Prime-Power Depth of Bent Partitions

Zhaorui Wu

A $p$-ary bent partition of $\mathbb{F}_p^n$ is a partition into $K$ nonempty cells such that every balanced assignment of its cells to $\mathbb{F}_p$ produces a bent function. It was asked whether every possible depth $K$ is a power of $p$; for general $p$...

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-08-28 arXiv

Explicit gauge-invariant variables in multifield inflation beyond linear order and Hamiltonian dynamics

Julien Grain, Hugo Holland, Lucas Pinol

General relativity coupled to multiple scalar fields is a diffeomorphism-invariant constrained system. Consequently, a naive counting of the perturbative degrees of freedom unavoidably overestimates the true number of physical modes propagating in the theor...

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 3.5 2026-08-28 arXiv

Are These Modules Worth Their Cost? A Paradigm-Level Accuracy-Cost Analysis of In-context Learning Text-to-SQL

Jiayan Lin, Yujia Liu, Zijin Hong et al.

Recent advances in in-context learning (ICL) text-to-SQL have substantially improved execution accuracy on public benchmarks by assembling increasingly elaborate pipelines around the base generator, yet existing studies typically report aggregate end-to-end...

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

verifier feedback
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-08-27 arXiv

Tacet: A Language and Type System for Automatic Statistical Validity Accounting

Chiké Abuah

Empirical comparisons between systems are a standard form of evidence in computer science research, but few are checked for statistical validity: most are never framed as statistical tests at all. Existing multiple-comparison procedures could control the re...

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

A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver

Haobo Ma, Wenlin Zhang, Manuel Israel Cázares

The SAIR Mathematics Distillation Challenge on Equational Theories asks a solver to classify whether one magma identity implies another and, for either verdict, to return a certificate accepted by a deterministic Lean judge. We present a single-file solver...

Why it matters Training signal: worth scanning for reward design, experience collection, or process supervision that could transfer to theorem proving.

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.

RL or distillation
Open PDF Semantic Scholar
15
adjacent score 1.9 2026-08-31 arXiv

Cubic-Root Gaussian Approximation under Unrestricted Covariance

Zijun Gao, Weihan Zhang

For Gaussian approximation over high-dimensional rectangles under unrestricted covariance, Chernozhukov et al. (2023b) conjectured that the $n^{-1/4}$ rate, up to logarithmic factors, is near-optimal. We show that, under the coordinatewise subexponential co...

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-08-27 arXiv

Zero-free columns in character tables of symmetric groups

Colin Defant, Sidharth Hariharan, Kenny Lau et al.

The rows and columns of the character table of the symmetric group $S_n$ are both naturally indexed by partitions of $n$. Let $D(n)$ denote the number of conjugacy classes of $S_n$ whose column contains no zero entry. The identity column is always zero-free...

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-08-27 arXiv

Proof of the Lyons--White Conjecture

Colin Defant, Ken Ono

Let $D_n$ be the dihedral group of order $2n$. Consider a continuous-time random walk on $D_n$ driven by arbitrary symmetric rates whose support generates $D_n$. For $p\in[1,\infty]$, we say the pair $(D_n,p)$ is rate-monotonic if for each fixed time $t$, t...

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

leanprover-community/mathlib4: chore: update Mathlib dependencies 2026-09-06 (#43495)

mathlib-update-dependencies[bot]

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

leanprover-community/mathlib4: chore(scripts): update nolints.json (#43474)

mathlib-nolints[bot]

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

leanprover-community/mathlib4: feat(Order/OrderIsoNat): every chain is finite when `<` and `>` are well-founded (#42633)

Snir Broshi

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

leanprover-community/mathlib4: feat(Combinatorics/SimpleGraph/Maps): `(f : H →g G) → H.map f ≤ G` (#43347)

Snir Broshi

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

leanprover-community/mathlib4: feat(Combinatorics/SimpleGraph/Finite): the `Fintype` instance for `incidenceSet` doesn't need `DecidableEq` (#41713)

Snir Broshi

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

leanprover-community/mathlib4: feat(CategoryTheory/Presentable): accessible functors satisfy the solution set condition (#41236)

Joël Riou

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