AI4Math

3core

17adjacent

70downweighted

0warnings

Today's Scan

Start with When Does Structured Knowledge Help Neural Theorem Proving?, then Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation. 20 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv20

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 6.5 2026-09-28 arXiv

When Does Structured Knowledge Help Neural Theorem Proving?

Sareh Nabi, Roland Vogl, Marzieh Nabi

Does structured mathematical knowledge help LLMs prove theorems in Lean 4? If so, for which models, and does the answer vary by problem? Formal libraries such as Mathlib encode 285,000+ verified theorems with syntactic dependencies, but the semantic layer m...

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

Lean proof agentsmathlib search

Open PDF Semantic Scholar

core score 6.5 2026-09-27 arXiv

Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation

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

Contemporary neural inference architectures rely on dense floating-point weight matrices stored in high-bandwidth memory (VRAM), incurring severe memory-wall bottlenecks and preventing native execution inside deterministic virtual machines like the Ethereum...

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

Formalising Linear Elliptic PDE Theory in Lean 4

Alejandro José Soto Franco, Kobe Marshall-Stevens

We formalise in Lean 4, on top of Mathlib, the solvability of the Dirichlet problem for second-order linear elliptic operators in divergence form. The machine-verified results, with no sorry in the development, include the Poincaré inequality, the existence...

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

Lean proof agentsmathlib search

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

adjacent score 3.5 2026-09-29 arXiv

GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research

Shuangping Li, Peng Zhang

We present GenLimitLib, a source-aligned Lean 4 library for language generation in the limit. Introduced by Kleinberg and Mullainathan at NeurIPS 2024, language generation in the limit studies a theoretical question motivated by LLMs: how to generate valid...

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

Session Type State Spaces Form Lattices

Alexandre Zua Caldeira

We prove that the state space of every well-formed session type, quotiented by strongly connected components, forms a bounded lattice; n-ary parallel composition yields product lattices. Two consequences follow: duality preserves the lattice up to isomorphi...

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

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

Christoph Benzmüller

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its proper...

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

Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms

Jaewook J. Suh, TaeHo Yoon, Edward Duc Hien Nguyen et al.

This paper presents Peppy, an AI-assisted workflow for discovering tight, analytic convergence proofs for first-order optimization algorithms. Generic approaches to using LLMs to conduct mathematical research target an unspecified, broad spectrum of problem...

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

Moments of random multiplicative functions with polynomial coefficients

Xinyu Wang

Let $f$ be a Steinhaus random multiplicative function and let $g$ be a polynomial of degree $d$. Write $S_N=N^{-1/2}\sum_{n\le N}f(n)\,e(g(n))$. We prove a quantitative dichotomy for the moments of $S_N$: for each integer $s\ge 2$, either $\mathbb{E}|S_N|^{...

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

Blackwell Boundaries

Shuo Li Liu

We give a finite simplex theorem. When the number of states equals the number of source signals and the source posterior likelihood-ratio vectors form a simplex, Blackwell dominance is characterized by a universal barycentric-coordinate condition. We also g...

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

adjacent score 3.5 2026-09-28 arXiv

A negative answer to Erdős Problem #786

Shisheng Li

Call a set $A$ of positive integers admissible if, whenever $a_1\cdots a_r=b_1\cdots b_s$ with $a_1,\dots,a_r$ distinct elements of $A$ and $b_1,\dots,b_s$ distinct elements of $A$, necessarily $r=s$. Erdős asked whether admissible sets can have density $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.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-27 arXiv

More than 83.69% of the zeros of the Riemann zeta function are distinct

Kristian Muri Knausgård

The lower asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, counted with multiplicity, is at least $0.8369928814\ldots$. The previous bound was $0.83625\ldots$. As in the proof of that bound, an unconditional version of Montgo...

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

Watch Later

Adjacent formalization or infrastructure signals. Keep them in peripheral vision unless they match an active project.

adjacent score 3.5 2026-09-27 arXiv

Formalization of the Galerkin Construction for the Two-Dimensional Navier--Stokes Equations in Lean

Weinan Wang

We formalize in Lean 4 the Galerkin construction of global Leray--Hopf weak solutions for the unforced two-dimensional Navier--Stokes equations on arbitrary bounded open domains with no-slip boundary conditions. For every initial datum in the solenoidal \(L...

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

The Same and Not the Same: A Machine-Checked Genealogy of Photochemical Theory

Junyi Gong, Zijie Qiu, Ben Zhong Tang

Chemistry's phenomenological theories multiply with its observables: the same physical reality is repeatedly named in different measurement contexts, and the relations among theories have never had an auditable carrier. Here we present PhotoLean, a machine-...

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

Predicting the Next State Is Not Enough: JEPA Representations for Lean Theorem Proving

Aarnav Choudhary

Neural theorem provers must both propose tactics and decide which valid successor states to explore. We study whether one-step Lean transitions provide a self-supervised signal for branch ordering. A JEPA-style model predicts latent successor representation...

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

adjacent score 3.5 2026-09-26 arXiv

Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs

Jorryt de Jong, Stefan Moraca, Ettore Cesari et al.

Large Language Models (LLMs) are highly capable of natural language reasoning and appear to store a great deal of lexical knowledge, but it is still unclear how much of this knowledge they actually use when reasoning, and whether they use it in the right wa...

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

AltGDA Achieves Global $O(1/T)$ Ergodic Convergence in Matrix Games

Tianlong Nan, Garud Iyengar, Christian Kroer et al.

Alternating gradient descent-ascent (AltGDA) is a simple and practically effective method for solving finite two-player zero-sum matrix games. However, the theory of AltGDA remains limited: existing results either apply only to unconstrained settings or req...

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 1.9 2026-09-28 arXiv

Uniqueness of four-body convex central configurations for all masses

Tejasvi Singh Tomar

We prove that for every choice of four positive masses and every cyclic ordering of the bodies there is exactly one strictly convex planar central configuration with that ordering, up to similarity. This answers Problem 10 in the list of Albouy, Cabral and...

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

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

negative score 0.8 2026-09-30 GitHub

leanprover/lean4: perf: reduce grind e-matching aggressiveness (#15414)

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

negative score 0.8 2026-09-30 GitHub

leanprover/lean4: fix: `grind` hom hooks fail on `let`-bound literals (#15417)

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

negative score 0.8 2026-09-30 GitHub

leanprover/lean4: chore: make nestedDeciable test more robust (#15413)

Paul Reichert

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

leanprover-community/mathlib4: refactor(SetTheory/ZFC): make `Class` an `abbrev` for `Set ZFSet` (#43467)

Yaël Dillies

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

leanprover-community/mathlib4: refactor(Algebra/Group): fix the definition of torsion-free non-abelian groups (#42407)

Thomas Browning

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

leanprover-community/mathlib4: fix(GroupTheory/Subgroup/Center): make the additive version of commGroupOfCenterEqTop instance_reducible (#44120)

Xavier Roblot

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

leanprover-community/mathlib4: feat: restricted multivariate power series as its own type and some missing API lemmas (#42867)

William Coram

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

leanprover-community/mathlib4: feat: in characteristic 0, precomposition by a linear map is analytic on the space of alternating maps (#43338)

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

Source Health

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

None