Daily field radar

AI4Math Radar

Start with MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize, then Prove2Me: An Open Collaborative Platform for Scaling Math Formalization. 20 fresh useful item(s) are inside the 21-day content window.

2026-08-31
Latest Newer Older
America/Los_Angeles Generated 2026-08-31T21:00:24Z JSON data
5core
15adjacent
69downweighted
0warnings

Today's Scan

Start with MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize, then Prove2Me: An Open Collaborative Platform for Scaling Math Formalization. 20 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv20

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

MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize

Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu et al.

Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent...

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.

AI math reasoningLean proof agents
Open PDF Semantic Scholar
2
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
3
core score 6.5 2026-08-26 arXiv

ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving

Wenqian Ye, Ziwei Guan, Eric Xie et al.

Automated theorem proving offers a natural foundation for recursive self-improvement in scientific discovery. However, existing neural provers do not fully preserve this recursive structure, where the learning process should be self-improving over time. Exi...

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 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
core score 6.5 2026-08-25 arXiv

Teaching Geometric Proof with Tech: Pitfalls and Possibilities

Hwei-Shin Harriman, Wode Ni, Yuchen Jin et al.

Geometric proof is a foundational yet challenging topic in mathematics, requiring students to integrate visual, logical, and notational skills. While technology has enhanced learning in other mathematical domains, its impact on geometric proof remains limit...

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.

Lean proof agentsverifier feedback
Open PDF Semantic Scholar
5
core score 6.5 2026-08-24 arXiv

A deterministic sin^2-type algorithm for complex cubic irrationalities with exact periodicity certificates

Ludovic Tagnon

Hermite asked in 1848 for a representation of real numbers whose eventual periodicity characterizes cubic irrationals. The totally real case was solved by Karpenkov's $\sin^2$-algorithm; the complex case, signature (1,1), is his Problem 4. We study a determ...

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
6
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
7
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
8
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
9
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
10
adjacent score 3.5 2026-08-27 arXiv

A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations

Floris van Doorn, Polona Durcik, Joris Roos et al.

This blueprint serves as a companion to a forthcoming, shorter traditional mathematical paper. The purpose of this blueprint is two-fold: first, it has served as the foundation for a formalization in Lean 4 of these results. This formalization has been comp...

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

The Kernel Deficit Dominates Twice the Hull Deficit: A Sharp Strengthening of Nakano's Inequality

Dakota Charles Baker

A point lies in the kernel of a polygon if it can see the entire polygon. Thus the kernel measures how much of the polygon is available to a single guard, while the convex hull measures how far the polygon is from being convex. We prove that these two losse...

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

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

Designability of RNA Targets with Up to Two Length-2 Helices

Ashutosh S. Jogalekar

RNA inverse folding asks for an RNA sequence whose prescribed secondary structure is the unique maximum-base-pair compatible fold. In the four-letter Watson-Crick model (A-U and C-G pairs only, no pseudoknots, and zero minimum base-pair span), Hales et al....

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

A dual reformulation of the complex sin^2-algorithm: exact identities, descent, and finiteness

Ludovic Tagnon

We develop the structure theory of the deterministic $\sin^2$-type algorithm for complex cubic fields introduced in the companion paper, addressing the complex-signature case of Karpenkov's Problem 4. The selection rule is shown to be, exactly, the minimiza...

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
14
adjacent score 3.5 2026-08-24 arXiv

Relative formalization in Isabelle/HOL of a result in inverse problems

Cătălin I. Cârstea

This reports on an experiment in autoformalization of arxiv:2606.15977, an inverse problems result for piecewise polynomial anisotropic conductivities, using Isabelle/HOL. The proof of the result is relative to a number of external results which were deemed...

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

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.

autoformalization
Open PDF Semantic Scholar
15
adjacent score 3.5 2026-08-24 arXiv

Multi-Winner Voting with Argumentative Ballots

Ryuta Arisaka, Hirotaka Ono

We introduce multi-winner voting with argumentative ballots (MVArg) and investigate theoretical properties. As our conceptual contribution, we generalise approval ballots to argumentative ballots, thereby allowing voters to express defeasible preferences ov...

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
16
adjacent score 3.5 2026-08-24 arXiv

Improved bounds for the smallest 4-chromatic graph of girth six

Glauco Rampone

For integers $k,g \ge 3$ let $n_g(k)$ denote the minimum order of a graph with chromatic number $k$ and girth at least $g$. Exoo and Goedgebeur (DMTCS 2019) proved $26 \le n_6(4) \le 66$; their 66-vertex witness has remained the smallest known 4-chromatic g...

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
17
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
18
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 69 low-priority match(es), folded for daily reading.
1
negative score 0.8 2026-08-31 GitHub

leanprover/lean4: perf: avoid `setTransparency` when the transparency is already in effect (#14967)

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
2
negative score 0.8 2026-08-31 GitHub

leanprover/lean4: fix: use the correct calling convention when over-applying a closure in `lean_apply_m` (#14969)

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
3
negative score 0.8 2026-08-31 GitHub

leanprover/lean4: feat: characterize when T-division equals zero (#8204)

Siddharth

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

leanprover/lean4: feat: add `Repr` instance for `Vector` (#14545)

Kitamado

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

leanprover/lean4: chore: update stage0

Lean stage0 autoupdater

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

leanprover-community/mathlib4: refactor(Tactic/Linter): rename and generalize `linter.style.nativeDecide` to `linter.style.native` (#43194)

DavidLedvinka

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

leanprover-community/mathlib4: feat: homogenization of an affine space (#39368)

Attila Gáspár

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