Daily field radar

AI4Math Radar

Start with MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize, then ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving. 18 fresh useful item(s) are inside the 21-day content window.

2026-08-30
Latest Newer Older
America/Los_Angeles Generated 2026-08-30T18:44:38Z JSON data
5core
13adjacent
71downweighted
0warnings

Today's Scan

Start with MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize, then ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving. 18 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv18

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

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

A Lean 4 Verification Report for Subregular Affine Cells and the Level $-1$ Vertex Algebra of Type $D$

Sihai Jin

We report a Lean 4 formal verification accompanying the paper "Subregular Affine Cells and the Level -1 Vertex Algebra of Type D" (arXiv:2608.11997). The formalization kernel-checks substantial internal parts of the proof architecture, including the Section...

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

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

ATHENA: Knowledge-guided agentic neural architecture search for AutoFormer-based electronic health record modeling

Deyi Li, Qi Xu, Lingyao Li et al.

Transformer-based models are widely used for clinical prediction from electronic health records (EHRs), yet their architectures require manual tuning, and the optimal configuration may vary across tasks and hospitals. Neural architecture search (NAS) automa...

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 Save for later unless the title matches your current proof-agent work.

verifier feedback
Open PDF Semantic Scholar
15
adjacent score 3.5 2026-08-21 arXiv

AI with Authority, from Application to Silicon

Jason Hickey

For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI inverts this relationship: at AI speed, machine verification is not only economical but essential to productiv...

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
16
adjacent score 1.9 2026-08-26 arXiv

The Birthday Paradox for non-backtracking walks on regular graphs

Benjamin Dozier

We show a birthday paradox for random non-backtracking walk on regular graphs of degree at least $3$: such a walk of length $k$ has high probability of self-intersecting when $k$ is significantly greater than $\sqrt n$, where $n$ is the number of vertices o...

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

FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence

Ziyu Wang, Qiming Dai, Yishan Wu et al.

Large language models can now generate complex, multi-step mathematical proofs, but reliably determining their correctness and localizing early logical errors remains a critical challenge. Existing evaluation approaches largely depend on model-based natural...

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

The General Subgroup Permanental-Dominance Conjecture in Order Four

Siwei Zeng

The general subgroup permanental-dominance conjecture was previously known only through matrix order three. This paper proves its complete order-four case: for every subgroup $H\leq S_4$, every irreducible complex character $χ$ of $H$, and every $4\times 4$...

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

leanprover/lean4: fix: more primitives for challenge (#14972)

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

leanprover/lean4: fix: app elaborator infotrees should have context when there is ambiguity (#13815)

Kyle Miller

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

leanprover-community/mathlib4: feat(RingTheory/PowerSeries/Log): log and exp as inverses (#37848)

Ralf Stephan

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
4
negative score 0.8 2026-08-30 GitHub

leanprover-community/mathlib4: feat(CategoryTheory): right Kan extensions and Guitart exact squares (#43063)

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
6
negative score 0.8 2026-08-30 GitHub

leanprover-community/mathlib4: chore: remove outdated adaptation notes after #42161 (#42745)

Jovan Gerbscheid

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

leanprover-community/mathlib4: chore: remove `CommRingCat.of` in AlgebraicGeometry\Modules\Tilde.lean (#42694)

Brian Nugent

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

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

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

Source Health

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

  • None