AI4Math

3core

13adjacent

72downweighted

0warnings

Today's Scan

Start with MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement, then Vero: Can AI Agents Build Formally Verified Software Repositories?. 16 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv16

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 12.3 2026-08-14 arXiv

MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

Lushi Pu, Weiming Zhang, Xinheng Xie et al.

Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to th...

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.

autoformalizationLean proof agentsRL or distillationtool-use agentsverifier feedback

Open PDF Semantic Scholar

core score 7.7 2026-08-13 arXiv

Vero: Can AI Agents Build Formally Verified Software Repositories?

Zhe Ye, Hantao Lou, Yuechun Sun et al.

AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a st...

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 agentsseed author: Kaiyu Yangverifier feedback

Open PDF Semantic Scholar

core score 6.5 2026-08-11 arXiv

GraphAlignCoder: Aligning Program and Proof Graphs for Code Generation

Yueke Zhang, Zihan Fang, Kevin Leach et al.

Code large language models (LLMs) can generate syntactically plausible programs that nevertheless violate hidden semantic constraints. Existing execution-feedback training methods identify whether a completed program fails, but provide limited supervision 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 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.

adjacent score 4.9 2026-08-11 arXiv

On Ishiki's Conjecture: $\mathrm{Met}(D)$ Is Not Completely Metrizable for $\lvert D\rvert=\aleph_1$

Tomoki Uda

For a discrete topological space $D$, let $\mathrm{Met}(D)$ denote the set of metrics on $D$ that are compatible with the discrete topology, equipped with the topology induced by the supremum distance. Ishiki's Conjecture 5.1 asserts that $\mathrm{Met}(D)$...

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

adjacent score 4.9 2026-08-11 arXiv

FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups

Tianjiao Nie, Ao Zhang, Yusen Tang et al.

Large-scale formalization of advanced mathematics requires more than translating individual statements: it must reconstruct a coherent theory distributed across heterogeneous sources. This process raises four challenges: discovering implicit dependencies, c...

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.

tool-use agentsverifier feedback

Open PDF Semantic Scholar

adjacent score 4.9 2026-08-10 arXiv

Power law graph attention: exact generalization of scaled dot-product attention, empirical collapse at inference

Burc Gokden

The Large Language Model from Power Law Decoder Representations (PLDR-LLM) and its attention, Power Law Graph Attention (PLGA), replace the fixed bilinear form of scaled dot-product attention (SDPA) with a learned, input-generated bilinear operator $G_{LM}$...

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

adjacent score 3.5 2026-08-14 arXiv

Audience capture, selective exposure, affective assimilation or ideological sorting? Polarisation of climate politics under low media-party parallelism

Arttu Malkamäki, Antti Gronow

Studies often attribute the polarisation of climate politics in majoritarian democracies to differing treatment of climate change by conservative and liberal media. How then does such polarisation occur in a system, where mainstream media do not systematica...

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

The transversal achievement game on a square grid

Kevin Guan

In the transversal achievement game on the $n\times n$ board, two players alternately claim cells, and the first to own a transversal---a set of $n$ cells of which no two share a row or column---wins. Ranđelović showed that the first player wins for every $...

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

adjacent score 3.5 2026-08-13 arXiv

More than two thirds of the zeta zeros are simple and on the critical line

Levent Alpöge, Ralph Furman

We prove unconditionally that at least two thirds of the nontrivial zeros of the Riemann zeta function, counted with multiplicity, are simple and lie on the critical line, and that at least five sixths are distinct; the previous unconditional records are $\...

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

Sharp Berry-Esseen Bounds for the Log Determinant of a Gaussian Sample Correlation Matrix

Hongru Zhao

Let $\widehat R$ be the Pearson sample correlation matrix formed from $n$ independent Gaussian observations in $p$ dimensions, and write $m=n-1\ge p$. Under the null correlation $R=I_p$, the classical independent beta product, exact cumulants, and full Four...

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

Grothendieck's theorem for Bessel sequences

Lukas Liehr, Mitchell A. Taylor, Peiyang Yu

We establish a sharp version of Grothendieck's theorem for Bessel sequences. Precisely, given a Bessel sequence $\{ x_j \}_{j\in\mathbb{N}}$ with Bessel bound $1$ in a Hilbert space, we show that there exists functions $\{ f_j \}_{j\in\mathbb{N}}$ belonging...

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

Non-Existence of EFX Chore Allocations for Monotone Cost Functions with Binary Marginals

Zehan Lin, Shengxin Liu, Biaoshuai Tao et al.

We study the existence of envy-free up to any item (EFX) allocations of indivisible chores when agents have monotone cost functions with binary marginals. For indivisible goods, the corresponding existence question is known to have an affirmative answer for...

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.

adjacent score 3.5 2026-08-11 arXiv

A Quantum Roadmap for Softmax Attention: Exact Born-Rule Analogs for Softmax Attention on the Probability Simplex

Eric A. F. Reinhardt, Adam J. Hauser

The attention mechanism forms the foundation of many modern AI models such as the Transformer. In one subclass of problems where attention is used, inputs and outputs are bound to the probability simplex so that all outputs sum to one. In this setting, soft...

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

On the Renormalization in Conformal Quantum Gravity

Ioseph L. Buchbinder, Petr M. Lavrov, Thomas M. Sangy et al.

One-loop divergences in classically conformal theory in curved spacetime is a nontrivial issue if the theory under consideration possesses gauge invariance. In this case, quantization involves introducing the gauge-fixing term and the action of ghosts, both...

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

adjacent score 2.9 2026-08-10 arXiv

P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation

Zenan Li, Ziran Yang, Peiyang Song et al.

Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouple...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

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.

seed author: Kaiyu Yangseed author: Ziran Yang

Open PDF Semantic Scholar

adjacent score 1.7 2026-08-11 arXiv

FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation

Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh et al.

Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these systems. Existing approaches require expensive human-annotated ground truth, or...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

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.

seed author: Wenda Li

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.

negative score 0.8 2026-08-17 GitHub

leanprover/lean4: perf: improve proof-over-applied cases in `ToLCNF` (#12814)

Robin Arnez

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

negative score 0.8 2026-08-17 GitHub

leanprover/lean4: feat: meta-programming changes ahead of #8309 (#10935)

Robin Arnez

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

negative score 0.8 2026-08-17 GitHub

leanprover/lean4: feat: lake: dependency partial clones (#14782)

Mac Malone

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

negative score 0.8 2026-08-17 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

negative score 0.8 2026-08-17 GitHub

leanprover-community/mathlib4: refactor(Analysis/Asymptotics): use `Monotone` predicate in `LinearGrowth` lemmas (#42700)

Nathanael Thompson

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

leanprover-community/mathlib4: fix(Cache): give each cache process its own temporary file names (#42752)

Kim Morrison

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

leanprover-community/mathlib4: feat: lifting a `Finsupp` to a quotient (#42864)

Michael Rothgang

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

leanprover-community/mathlib4: feat: add formula for the `j`-invariant of an elliptic curve (#41504)

Paul Lezeau

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