AI4Math

3core

10adjacent

77downweighted

0warnings

Today's Scan

Start with AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics, then Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback. 13 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv13

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

AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics

Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund et al.

Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring th...

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

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

Open PDF Semantic Scholar

core score 6.5 2026-08-31 arXiv

Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback

Gregory Morse

Classical lower bounds show that multiplying two degree-three polynomials over $\mathbb F_2$ requires nine scalar products in bilinear or quadratic models. They do not settle unrestricted Boolean multiplicative complexity: an XOR--AND circuit may reuse nonl...

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

SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Hojae Han, Jongyoon Kim, Sanghyeok Park et al.

Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean. A central challenge is that current evaluation metrics can accept type-correct but misaligned statements or reject correct statements written in a diffe...

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

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 agents

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

AutoGraphForge: Towards Automated Graph Theory Discovery

Ján Pastorek

We report on our ongoing project to develop a computational pipeline, AutoGraphForge, for an automated graph-theoretic conjecturing-refuting-formalizing-proving system. Conjecture generation is counterexample-guided and runs in rounds: a Graffiti3 generator...

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

adjacent score 4.9 2026-08-30 arXiv

The S-matrix conjecture

Yinjie Li

Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix $A\in\mathbb R^{n\times n}$ satisfies $\|A^{-1}\|_F\ge 2n(n+1)^{-1}\|A\|_{\max}^{-1}$, with equality precisely for positive multiples of $S$-matrices. Cheng proved the conject...

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

Separating Parsing Expression Grammars using Cell-Probe Lower Bounds

Jungyeom Kim, Jihyeok Park

We resolve three open problems concerning parsing expression grammars (PEGs). We construct a single language $C$ satisfying $C\in\mathsf{LIN}\cap\mathsf{PEG}$ and $C^R\in\mathsf{LIN}\setminus\mathsf{PEG}$. This proves that some linear context-free language...

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

Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free

Maher Kallel, Mohamed El Louadi

In May 2026 an OpenAI model produced a counterexample to the Erdős unit distance conjecture. Five mathematicians published a human-verified version the same day, and the result entered the literature within weeks. In August 2026 the same laboratory publishe...

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

A Counterexample to a Problem of Pommerenke on Convex Functions in the Class $Σ$

Yuankai Guo, Xiaozhe Hu

Let $Σ$ denote the class of functions $f(z) = z + b_0 + b_1 z^{-1} + \cdots$ that are analytic and univalent in the exterior unit disk $Δ^* = \{z \in \mathbb{C} : |z| > 1\}$. In 1962, Ch. Pommerenke proved that if $F$ and $G$ are convex functions in $Σ$, th...

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

SparseStack Is an Optimal Oblivious Subspace Embedding

Diar Heidary

The fully independent SparseStack sketch is a vertical stack of $s$ independent CountSketch matrices, scaled by $s^{-1/2}$, so that every column has exactly $s$ nonzero entries. We prove that it is an oblivious subspace embedding for $d$-dimensional subspac...

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

Colombo's Determinant Problem

Qianli Ma

We completely solve Colombo's 1928 determinant problem. For distinct real $x_1,\ldots,x_N$, $N\geq 2$, and an integer $D\geq 1$, we prove that $\det[(x_j-x_i)^D]\neq 0$ if and only if $D\geq N-1$ and either $N$ is even or $D$ is even. The even-exponent case...

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

Purely Periodic Three-move Subtraction Games

Hikaru Manabe

A subtraction game is played on a heap of tokens. The players take turns removing s tokens for some s in a fixed set S of positive integers, and the player who cannot move loses. The sequence of Sprague-Grundy values of such a game is eventually periodic. W...

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

adjacent score 1.9 2026-09-01 arXiv

A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver

Haobo Ma, Wenlin Zhang, Manuel Israel Cázares

The SAIR Mathematics Distillation Challenge on Equational Theories asks a solver to classify whether one magma identity implies another and, for either verdict, to return a certificate accepted by a deterministic Lean judge. We present a single-file solver...

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

RL or distillation

Open PDF Semantic Scholar

Watch Later

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

adjacent score 1.9 2026-08-31 arXiv

Cubic-Root Gaussian Approximation under Unrestricted Covariance

Zijun Gao, Weihan Zhang

For Gaussian approximation over high-dimensional rectangles under unrestricted covariance, Chernozhukov et al. (2023b) conjectured that the $n^{-1/4}$ rate, up to logarithmic factors, is near-optimal. We show that, under the coordinatewise subexponential co...

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

negative score 0.8 2026-09-07 GitHub

leanprover/lean4: feat: enable checking lean4export via leanchecker (#15050)

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

leanprover/lean4: feat: add `lake check` to check a project against external checkers (#14990)

Sebastian Ullrich

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

leanprover-community/mathlib4: refactor(RingTheory/Localization): restore IsLocalization.surj' (#42967)

Yi.Yuan

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

leanprover-community/mathlib4: refactor(Geometry): remove unnecessary hypothesis (#43444)

Laurance

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

leanprover-community/mathlib4: perf(Tactic/Linter/InternalConstructor): try `foldInfo` instead of `foldInfoM` (#43431)

Anne Baanen

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

leanprover-community/mathlib4: feat(Topology/Separation/Hausdorff): add `tendsto_nhds_unique_of_forall` (#42986)

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

leanprover-community/mathlib4: feat(RingTheory/PowerSeries): coeff of a power series times a numeral (#42252)

Bhavik Mehta

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

leanprover-community/mathlib4: feat(RingTheory/Ideal): generalize span_singleton_dvd_span_singleton_iff_dvd and emultiplicity_eq_emultiplicity_span (#40557)

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

Source Health

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

None