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. 15 fresh useful item(s) are inside the 21-day content window.

2026-10-05
Latest Newer Older
America/Los_Angeles Generated 2026-10-05T22:08:43Z JSON data
2core
13adjacent
74downweighted
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. 15 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv15

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 3.5 2026-10-02 arXiv

Law And Order: Tax Law Autoformalization

Sophia Simeng Han, Yoshiki Takashima, Anjiang Wei et al.

Legal systems are increasingly implemented through software, yet scalable methods for translating legal texts into accurate symbolic representations remain underdeveloped. We study this problem through tax law, where forms and filing instructions define lar...

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

High-Rate Quantum Codes with Proven Distance and Low-Weight Measurements

Kishor Bharti, Tobias Haug, Runzhou Tao et al.

We study a family of quantum subsystem codes defined on rectangular coordinate grids of any dimension, with even side lengths of at least four. The directly measured operators act along coordinate lines. For every member of the family, we derive the number...

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

Greedy Uniformity on Trees: Exact Obstruction and Near-Uniform Spiders

John Fairfax-Ball

Choose a uniformly random ordering of the vertices of a finite tree and run the usual greedy maximal-independent-set algorithm. We compare the resulting law on maximal independent sets with the uniform law. We prove that exact uniformity occurs only for the...

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-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
11
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
12
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

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

leanprover/lean4: fixup checker

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

leanprover/lean4: fix: stop consuming newlines for role and inline code recovery (#15495)

David Thrane Christiansen

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

leanprover/lean4: fix: prevent `Loop.configure` leaks and `System.random` size limits, `Loop.alive` and system error handling (#15175)

Sofia Rodrigues

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

leanprover/lean4: fix: fold orphan raw `Nat` literals in `Sym.simp` (#15483)

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

leanprover/lean4: fix: encode products by large numerals in `grind hom` with a small complement coefficient (#15482)

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

leanprover/lean4: fix: do not run non-stateful linters on invalid commands (#15485)

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

Source Health

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

  • None