Daily field radar

AI4Math Radar

Start with SkillEvoLean: Mutation-enhanced skill evolution for Lean provers, then LeanSide: A Formally Verified Co-Reasoning System for Natural-language Proofs. 18 fresh useful item(s) are inside the 21-day content window.

2026-10-03
Latest Newer Older
America/Los_Angeles Generated 2026-10-03T18:47:27Z JSON data
2core
16adjacent
72downweighted
0warnings

Today's Scan

Start with SkillEvoLean: Mutation-enhanced skill evolution for Lean provers, then LeanSide: A Formally Verified Co-Reasoning System for Natural-language Proofs. 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 12.3 2026-10-01 arXiv

SkillEvoLean: Mutation-enhanced skill evolution for Lean provers

Kuo Zhou, ZiXion Yang, Lu Zhang

Skill evolution offers a promising way to improve large language model agents without updating their parameters, but its use in formal theorem proving remains underexplored. Existing methods mainly target natural-language reasoning, improving skills by anal...

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 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 9.5 2026-09-30 arXiv

LeanSide: A Formally Verified Co-Reasoning System for Natural-language Proofs

Chenjun Guo, Manooshree Patel, Arnav Mehta et al.

Large language models are increasingly used as collaborators on deductive-reasoning tasks, but their outputs can hallucinate or pull users away from intended reasoning. Formal proof assistants provide machine-checked verification, but have a steep learning...

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
adjacent score 4.9 2026-10-01 arXiv

Fewer Tokens, Better Action: GPT-6 Astra Robot Agents with 14% Higher Success Rate but 65% Fewer Tokens

Ruiyang Si, Jianxin Bi, Shunyu Yang et al.

Vision language model (VLM) agents can control robots through visual feedback and action primitives, but repeated model invocations and redundant observations incur substantial token overhead. We introduce PyRUA-Lean, an interactive code-execution framework...

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.

tool-use 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-10-01 arXiv

Borcea's 2-variance conjecture

Teng Zhang

In this paper, we prove Borcea's 2-variance conjecture. The Lean 4 formalization of the main results are also provided.

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
5
adjacent score 4.9 2026-10-01 arXiv

Baernstein's quasi-norm monotonicity conjecture for polynomials with unimodular zero

Teng Zhang

Let $m$ denote the normalized Haar measure on the unit circle $\mathbb{T}$. For $0<r<\infty$, define $\lVert f\rVert_{r}:=\left(\int_{\mathbb{T}}|f|^{r}\,\mathrm{d} m\right)^{1/r}$, with $\lVert f\rVert_{0}$ and $\lVert f\rVert_{\infty}$ interpreted as the...

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-10-01 arXiv

A proof of Lehmer's permutation conjecture for neighbor-swap graphs

Tom Verhoeff

In 1965, D. H. Lehmer conjectured that the permutations of every multiset admit an imperfect Hamiltonian traversal by adjacent swaps: a walk in the neighbor-swap graph that visits every word, with some words visited twice in order to reach a neighbor and re...

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

The Burr-Erdős-Graham-Sós conjecture for the seven-cycle

Asad Shahab

For a graph $H$, let $f(n,e,H)$ be the least number of colors in an edge-coloring of some $n$-vertex graph with at least $e$ edges in which every copy of $H$ is rainbow. Burr, Erdős, Graham, and Sós conjectured that $f(n,\lfloor n^2/4\rfloor+1,C_{2k+1})=(1/...

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-10-01 arXiv

Exact Distinguishability in Non-Markovian Decision Processes

Kabir Murjani, Nisarg Patel

Non-Markovian environments are often modeled as Regular Decision Processes (RDPs), where dynamics depend on the interaction history through a finite automaton. Existing offline guarantees for RDPs rely on a distinguishability assumption on the behaviour pol...

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-10-01 arXiv

Cost Comparisons for Random and Deterministic Scans in Component-Wise Markov Chains

Youngwoo Kwon

Gibbs samplers, and more generally component-wise Markov chain Monte Carlo algorithms such as Metropolis-within-Gibbs, can be implemented using either random-scan or deterministic-scan updates. How much convergence can depend on this choice of scanning rule...

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

Improved Tristate Multiplication With Formalization in Rocq

Nandakumar Edamana, Piyush P Kurur, Unnikrishnan Cheramangalath

We give a new multiplication algorithm for tristate numbers improving upon the state-of-the-art implementation from the Linux kernel in terms of precision and formal proofs. Our algorithm is significantly more precise as shown by experimental evaluation (at...

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

Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean

Jules Viennot, Guillaume Baudart, Marc Lelarge

Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with proof assistants such as Rocq or Lean through an interface that controls what t...

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

Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization

Wei Zhao, Yangshuo Zou, Chengxiang Ding et al.

We present FYAN, a human--AI harness for document-level mathematical formalization. Rather than treating theorems in isolation, FYAN coordinates an end-to-end workflow spanning specification, proof planning, logical review, Lean proof construction, knowledg...

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 if you are thinking about retrieval, premise selection, or library search.

mathlib search
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-09-30 arXiv

A Fourier-Label Information-Loss Barrier for Dihedral Coset Algorithms

Aparna Gupte, Seyoon Ragavan, Mark Zhandry

We establish a no-go theorem for a broad class of quantum algorithms for the dihedral coset problem (DCP). We consider the Fourier-sampling and subset-sum-measurement template proposed by Regev (SIAM Journal on Computing, 2004), which is one of the main app...

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-09-29 arXiv

Restricted Binomial GCDs at Primes Congruent to -1

John Fairfax-Ball

For integers $m\geq 2$ and $m\mid N$, let $G(N;m)=\gcd\{\binom{N}{k}:0<k<N,\ m\mid k\}$. We prove a complete $p$-adic valuation formula for $G(N;m)$ at primes $p\equiv -1\pmod m$, under the hypotheses $m\geq 3$, $m\mid N$, and $m<N$. Writing $N=\sum_i d_i p...

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

Machine-Checked Computational Group Theory in Lean 4: Operational Schreier-Sims Stabilizer Chains, BSGS Sifting, and Backtrack Ordered Partitions

Volkan Dağlı, Zerrin Dağlı, Dağhan Dağlı

We present gap-lean4-port (Release v0.2.0), a machine-checked formalization of foundational algorithms in computational discrete algebra and permutation group theory within the Lean 4 interactive theorem prover and Mathlib4. While modern proof assistants fe...

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

LeanPolish: Verified Supervision for Lean Proof Compression

Pauline Bourigault

Verified proof edits offer a natural source of supervision for improving language-model-generated Lean proofs. Yet verification establishes that an edit is correct, not that its training signal is free of search artifacts. We introduce LeanPolish, a symboli...

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
17
adjacent score 1.9 2026-10-01 arXiv

When Do Intrinsic Rewards Lead to Exploration?

Scott W. Viteri, Laura Gomezjurado Gonzalez, Clark Barrett

Intrinsic rewards are designed to guide exploration in reinforcement learning by assigning value to an agent's experience, for example through prediction error or learning progress. However, maximizing these rewards need not produce the most informative exp...

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 reward construction and whether failures provide dense learning signal.

Read if Save for later unless the title matches your current proof-agent work.

RL or distillation
Open PDF Semantic Scholar
18
adjacent score 1.9 2026-09-30 arXiv

Magnitude of module categories and special biserial algebras

Haruhisa Enomoto

Børve, Horiatakis, and Kalck defined the magnitude of the module category of a representation-finite algebra as the sum of the entries of the inverse of the matrix of Hom dimensions between indecomposable modules. They showed it is an Euler characteristic,...

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 72 low-priority match(es), folded for daily reading.
2
negative score 0.8 2026-10-03 GitHub

leanprover/lean4: perf: build library suggestion indexes with one parallel traversal (#15391)

Marcelo Lynch

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-10-03 GitHub

leanprover/lean4: fix: kernel error in `grind` on `Char.ofNat` numerals, and evaluate `Char` literals (#15448)

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
4
negative score 0.8 2026-10-03 GitHub

leanprover/lean4: fix: keep bit-vector literals in `OfNat.ofNat` form in the `Sym.simp`-based `grind` normalizer (#15458)

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
5
negative score 0.8 2026-10-03 GitHub

leanprover/lean4: feat: support `Fin.log2` and the `Nat`/`Int` casts into `Fin` in `grind`'s homomorphism rules (#15445)

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
6
negative score 0.8 2026-10-03 GitHub

leanprover-community/mathlib4: perf: speed up `FunLike` synthesis (#44317)

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-10-03 GitHub

leanprover-community/mathlib4: fix(MeasureTheory/Measure/Typeclasses/SFinite): typo in `SigmaFinite` docstring (#44410)

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

Source Health

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

  • None