AI4Math

2core

18adjacent

69downweighted

0warnings

Today's Scan

Start with Long-horizon autoformalization of a core theorem underlying MIP* = RE, then FloatLib: Verified Floating-Point Arithmetic in Lean. 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-17 arXiv

Long-horizon autoformalization of a core theorem underlying MIP* = RE

Sirui Lu, Ruixuan Deng, Yanqiao Zhu et al.

Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Dr...

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

autoformalizationLean proof agents

Open PDF Semantic Scholar

core score 6.5 2026-09-16 arXiv

FloatLib: Verified Floating-Point Arithmetic in Lean

Robert Joseph George, Will Adkisson, Anima Anandkumar

We present FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean 4 that combines broad format coverage, machine-checked correctness, and efficient certified execution. To our knowledge, FloatLib is the first Lean library to unif...

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for agents.

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

Open PDF Semantic Scholar

adjacent score 4.9 2026-09-16 arXiv

Beyond Sendov's conjecture: the quadratic Tang--Zhang inequality

Teng Zhang

Very recently, Lech Mazur proved the celebrated Sendov conjecture, and Terence Tao subsequently distilled the main ideas of the proof in a blog post. In this paper, we establish a quantitative strengthening of Sendov's conjecture, namely the quadratic Tang-...

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

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

Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194

Cameron Beeley

For a finite simple graph G, let alpha(G) denote its independence number and let l_avg(G) = (1 / |V(G)|) sum_{v in V(G)} alpha(G[N_G(v)]) be the average independence number of its open neighbourhoods. Written on the Wall II Conjecture 194 asserts that every...

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

LIMBO: Learning and Internalizing Model-Free Barrier Objectives for Agile and Safe Whole-Body Control

Jake Gonzales, Arturo Flores Alvarez, Yu-Ming Chen et al.

Safe whole-body control requires coordinating collision avoidance and balance under high-dimensional, nonlinear dynamics--making safety certificates difficult to design and reuse across behaviors. We present LIMBO, a framework for synthesizing a state-actio...

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

Improved bounds for universal convex covers of unit arcs

Ethan Keller

Moser's worm problem asks for a planar region of least area containing a congruent copy of every unit arc. We show that the infimum area $α$ among convex universal covers satisfies $0.239\leα\le0.24633\ldots$, reducing the gap between the previous refereed...

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

A lower bound for $\langle 3,2,m \rangle$ matrix multiplication

Askar Tsyganov, Uliana Parkina, Sergey Samsonov et al.

We prove that, over any field, the bilinear complexity of multiplying a $3\times 2$ matrix by a $2\times m$ matrix is strictly greater than $24m/5$. In particular, every exact bilinear algorithm for multiplying a $3\times 2$ matrix by a $2\times 5$ matrix r...

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

Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof

Maseeh Ghodsi

A Leech tree of order $n$ is a tree with positive integral edge weights whose $n(n-1)/2$ pairwise weighted distances are precisely $1,2,\ldots,n(n-1)/2$. This paper gives a computer-assisted proof that no Leech tree of order $18$ exists. The argument has 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-17 arXiv

LLVM Translation Validation Automated with Large Language Models and Lean

Chunhao Liao, Hongxu Xu, Xintong Zhou et al.

LLVM is the cornerstone of modern compilers, but its subtle intermediate representation (IR) semantics make transformations error-prone and necessitate formal verification. Alive2, a state-of-the-art translation validator based on satisfiability modulo theo...

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

A Mean-Field Approach for Safe Routing of Multi-Destination Urban Air Mobility Networks

Nameer Fawwaz Ahmed, Cody Fleming, Yasser Shoukry

As Urban Air Mobility (UAM) systems scale toward high-density operations, managing autonomous Unmanned Aerial Vehicle (UAV) traffic requires control frameworks that are both tractable and safety-critical. This paper presents a principled optimal control-the...

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 3.5 2026-09-16 arXiv

Descriptive Complexity in Lean: Completeness by First-Order Reductions

Pierre Senellart, Anton Gnatenko

We show that descriptive complexity can serve as a foundation for formalizing computational complexity results in a proof assistant, by constructing a Lean library centered around the following concepts: decision problems are isomorphism-invariant predicate...

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 if you are thinking about retrieval, premise selection, or library search.

mathlib search

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-16 arXiv

A Strongly Aperiodic Monotile in Three Dimensions

Ioannis Tsiokos

Socolar and Taylor asked for a single, simply connected three-dimensional prototile that forces nonperiodicity by shape alone, admitting no weakly nonperiodic tiling; the Schmitt-Conway-Danzer biprism and the three-dimensional Socolar-Taylor tile admit scre...

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

The Taub-NUT Metric Is Not Projectively Induced

Shaosai Huang

LeBrun's Kähler realization $g_m$ of the Taub--NUT metric on $\mathbb{C}^2$ is complete, Ricci-flat and not flat. Loi, Zedda and Zuddas proved that no multiple $αg_m$ admits a Kähler immersion into a finite- or infinite-dimensional complex projective space...

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

Rogers--Ramanujan identities from the geometry of $X^a=Y^b$

Yifeng Huang, Kenny Lau, Ken Ono

We prove the conjecture of Huang, Jiang, and Oblomkov (HJO) giving a geometric extension of the Rogers--Ramanujan and Andrews--Gordon identities for every torus-knot singularity $X^a=Y^b$ with coprime $1<a<b.$ For a prime power $q$, let $\mathcal{NC}_n^{a,b...

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

adjacent score 1.9 2026-09-17 arXiv

Paths maximize the expected range of graph-indexed random walks

Yinfeng Zhu

We prove that a path maximizes the expected range of a uniformly chosen graph homomorphism into the integers, with one vertex pinned at zero, among all connected bipartite graphs of the same order. This establishes the expectation form of the Benjamini--Häg...

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

adjacent score 1.9 2026-09-17 arXiv

A counterexample to the quantum Hedetniemi conjecture

Julius A. Zeiss

Godsil, Roberson, Šámal and Severini conjectured that the quantum chromatic number of the categorical product of two graphs equals the minimum of the quantum chromatic numbers of the factors. We disprove this conjecture: we construct explicit finite graphs...

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

adjacent score 1.9 2026-09-16 arXiv

On a conjecture of Browning and Sawin on random hypersurfaces with sign coefficients

Ken Ono, Ashvin Swaminathan

Browning and Sawin conjectured that random hypersurfaces with sign coefficients are smooth with probability tending to one as the degree grows. We prove this conjecture and obtain a quantitative bound. For each $n\geq1$, a degree $d$ form in $n+1$ variables...

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

adjacent score 1.9 2026-09-16 arXiv

A Walk From Free Probability to Matrix Discrepancy II: Weaver's Problem and the Kadison-Singer Conjecture

Tarun Kathuria

\cite{mss2015} proved Weaver's discrepancy result existentially, resolving the Kadison--Singer conjecture . Finding such signs efficiently for general inputs remained an open algorithmic question. In the real-arithmetic model, we give a deterministic algori...

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

negative score 0.8 2026-09-21 GitHub

leanprover/lean4: refactor: use `Sym.Arith` classification in the `grind` ring solver (#15190)

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

leanprover/lean4: perf: make ExplicitRC scope sensitive (#15251)

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

leanprover/lean4: perf: allow deriving values from any relevant let (#15256)

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

leanprover/lean4: fix: remove `withPtrEq` (#15252)

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

negative score 0.8 2026-09-21 GitHub

leanprover/lean4: fix: lake: track cached ltar from partial unpack (#15231)

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

leanprover/lean4: fix: better defeq error messages (#14537)

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

leanprover/lean4: feat: provide CaDiCaL via FFI (#15247)

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

leanprover/lean4: feat: add `Environment.realizationEnvContains` (#15237)

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

Source Health

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

None