AI4Math

8core

15adjacent

65downweighted

0warnings

Today's Scan

Start with Harnessing Code Agents for Automatic Software Verification, then Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics. 23 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv23

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.

core score 9.5 2026-07-07 arXiv

Harnessing Code Agents for Automatic Software Verification

Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs a...

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

core score 9.3 2026-07-07 arXiv

Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics

Pavel Snopov, German Magai

Recent advances in AI for Mathematics have focused largely on autoformalization and theorem proving, leaving the role of Computer Algebra Systems (CAS) in agentic LLM workflows underexplored. We propose a ReAct-style agentic setup that combines LLM reasonin...

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.

autoformalizationAI math reasoningverifier feedback

Open PDF Semantic Scholar

core score 7.9 2026-07-06 arXiv

FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

Haocheng Wang, Baiyu Huang, Yingjia Wan et al.

The veracious semantic alignment in autoformalization is significant for formal mathematical reasoning. However, existing evaluations provide only opaque binary verdicts or scalar scores, offering no interpretable insight into where or why translations fail...

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.

autoformalizationAI math reasoningverifier feedback

Open PDF Semantic Scholar

Worth Opening

Good candidates after the first three. These are plausible paper-tab opens, not a mandatory reading list.

core score 7.5 2026-07-08 arXiv

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

Eric Jiang, Xiao Liang, Yikai Zhang et al.

Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for well-defined mathematical problems through Interactive Theorem Proving (ITP) la...

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 Read if you have 5 minutes and want a direct AI4Math signal.

AI math reasoningLean proof agentsseed author: Nanyun Peng

Open PDF Semantic Scholar

core score 6.5 2026-07-09 arXiv

From Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game

Arthur F. Ramos, Tulio Soria

We present a metagame analysis of the competitive Pokemon Trading Card Game, machine-checked in Lean 4 over real tournament data. The headline game-theoretic results, including Nash equilibrium, replicator dynamics, and the matrix-level type-bridge computat...

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

core score 6.5 2026-07-07 arXiv

Stable Phase Retrieval for Spans of Independent Random Variables

Pedro Abdalla, Jaume de Dios Pont, João P. G. Ramos et al.

We prove that, after $L^2$ normalization, stable phase retrieval holds over the $L^2$-spans of independent real-valued centered random variables if and only if all but possibly one coordinate satisfies a uniform two-sided $L^1$ bound. This provides a comple...

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 Read if you have 5 minutes and want a direct AI4Math signal.

autoformalizationLean proof agents

Open PDF Semantic Scholar

core score 6.5 2026-07-05 arXiv

LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics

Ján Perháč, Vasyl Khashcha, Samuel Novotný

We present LogicProof, an interactive web-based theorem prover designed for educational use. The system supports natural deduction and sequent calculus for propositional and first-order logic in both classical and constructive variants. It emphasizes a mode...

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.

Lean proof agentsverifier feedback

Open PDF Semantic Scholar

core score 6.5 2026-07-04 arXiv

Neuro-Symbolic Reasoning for Vulnerability Detection

Yanjie Zhao, Hongjie Chen, Li Lu et al.

Ask a large language model (LLM) whether a pointer dereference is safe, and it can often produce a plausible justification for ``yes''. The difficulty is that a fluent justification is not a proof. This gap is precisely where automated vulnerability detecti...

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 Read if you have 5 minutes and want a direct AI4Math signal.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-07-07 arXiv

SCOPE: Leveraging Subgoal Critiques for Code Generation

Yueke Zhang, Yifan Zhang, Zihan Fang et al.

Code generation with large language models (LLMs) remains unreliable because generated programs can appear correct while still violating key semantic requirements in the natural language specification. Existing feedback-based methods improve over coder-only...

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 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 distillationverifier feedback

Open PDF Semantic Scholar

adjacent score 3.5 2026-07-09 arXiv

Cantor measures with odd base do not admit Fourier frames

Jaume de Dios Pont, Lukas Liehr, Mitchell A. Taylor

We prove that the Cantor measure with base $b$ does not admit a Fourier frame whenever $b > 1$ is an odd integer. In particular, this answers a question of Strichartz on the existence of a Fourier frame for the middle third Cantor measure. A formalization o...

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

adjacent score 3.5 2026-07-08 arXiv

Multi-agent Autoformalization of Tensor Network Theory

Sirui Lu, Erickson Tjoa, J. Ignacio Cirac

We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics, with the autoformalization of the fundamental theorem of matrix-product states as a demonstration. The a...

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

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.

autoformalization

Open PDF Semantic Scholar

adjacent score 3.5 2026-07-07 arXiv

Formalizing Scarf, Brouwer, and Nash in Lean

Yuwei Lyu, Kai Li

We formalize in Lean 4 a complete combinatorial route from Scarf's theorem to Brouwer's fixed point theorem and to the existence of mixed Nash equilibria in finite games. The development follows Ivanov's indexed-order formulation of Scarf's theorem, formali...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

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.

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.

adjacent score 3.5 2026-07-07 arXiv

Closed-form fractional radial links for elliptical Mahalanobis discriminant analysis

Serhii Zabolotnii

We study binary classification under shared-generator elliptical class-conditional distributions. The log-likelihood ratio is an additive function of the two squared Mahalanobis radii, with radial link $\varphi=\log g$; QDA is recovered only when this link...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

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.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-07-07 arXiv

Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean

Michael R. Douglas

Mathematicians have embraced interactive theorem provers with growing enthusiasm -- building large shared libraries and machine-checking a string of landmark results. Theoretical physics is different: most of its results are not theorems but justified by ar...

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

adjacent score 3.5 2026-07-06 arXiv

SPL: Orchestrating Workflows with Declarative Deterministic-Probabilistic Composition

Wen G. Gong

We present SPL (Structured Prompt Language), a declarative language that composes deterministic and probabilistic computation modes in a single specification. While existing frameworks separate these -- orchestration systems (AutoGen, CrewAI, LangGraph) for...

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

adjacent score 3.5 2026-07-06 arXiv

Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information

Kazumi Kasaura, Kei Tsukamoto, Kento Mori et al.

Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi relative entropy is a fundamental divergence with various applications, and its data processing inequality (DPI) under quantum channels is a cornerstone result. In...

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.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-07-05 arXiv

Mechanism-level routing failure in LLMs over Lean-verified algebraic structures

Manuel Israel Cázares, Wenlin Zhang, Haobo Ma

We present an empirical study of structural routing failure in large language models (LLMs) over a formally verified algebraic corpus. The task requires selecting the correct proof-mechanism label from a fixed closed template set for compact mathematical ob...

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

adjacent score 3.5 2026-07-03 arXiv

LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean

Simon Jeanteur, Lorenzo Veronese, Magdalena Solitro et al.

Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-de...

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

verifier feedback

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 65 low-priority match(es), folded for daily reading.

negative score 0.8 2026-07-12 GitHub

leanprover-community/mathlib4: feat(RingTheory/Ideal): prime avoidance for maximal ideal (#40814)

Nailin Guan

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

negative score 0.8 2026-07-12 GitHub

leanprover-community/mathlib4: feat(Algebra/GroupWithZero): prove that `Is{Left,Right}CancelMulZero` is Dedekind-finite (#41453)

Noah Walker

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

negative score 0.8 2026-07-12 GitHub

leanprover-community/mathlib4: chore: update Mathlib dependencies 2026-07-12 (#41650)

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

negative score 0.8 2026-07-12 GitHub

leanprover-community/mathlib4: chore: fix nsmul and zsmul non-reducible diamond in SplittingField (#40708)

Sebastien Gouezel

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

negative score 0.8 2026-07-12 GitHub

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

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

negative score 0.8 2026-07-12 GitHub

leanprover-community/mathlib4: chore(RingTheory/Polynomial/Basic): remove unused `haveI` and defeq abuse (#41608)

Yongle Hu

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

negative score 0.8 2026-07-12 GitHub

leanprover-community/mathlib4: chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor (#41550)

Scott Carnahan

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

negative score 0.8 2026-07-12 GitHub

leanprover-community/mathlib4: chore(Geometry/Manifold/ContMDiff/Atlas): generalise `mem_maximalAtlas_of_contMDiffOn` and friends (#40720)

mathlib-splicebot[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