AI4Math

6core

9adjacent

74downweighted

0warnings

Today's Scan

Start with OpenProver: Agentic and Interactive Theorem Proving with Lean 4, then TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs. 15 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv15

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 16.9 2026-07-10 arXiv

OpenProver: Agentic and Interactive Theorem Proving with Lean 4

Matěj Kripner, Milan Straka

In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates a Planner-Worker-Verifier architecture inspired by recent ATP agentic systems...

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

Lean proof agentstool-use agentsverifier feedback

Open PDF Semantic Scholar

core score 7.9 2026-07-13 arXiv

TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs

Burak S. Akbudak, Zeynel A. Uluşan, Can S. Erer et al.

Tree search algorithms enable systematic exploration of the proof space in neural theorem proving. Existing LLM tree search libraries primarily target natural language reasoning and do not provide native integration with formal verifiers, while theorem prov...

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

AI math reasoningLean proof agents

Open PDF Semantic Scholar

core score 7.9 2026-07-13 arXiv

Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization

Tian-Shuo Liu, Shiyuan Zhang, Zijie Geng et al.

Full-proof autoformalization bridges extensive mathematical proofs in natural language with formally validated reasoning, offering a pathway to elevate the ceiling of verifiable mathematical reasoning. Unlike statement-level formalization, proof autoformali...

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.

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 6.5 2026-07-10 arXiv

Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory

Chengkai Zhu, Ziao Tang, Guocheng Zhen et al.

Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block...

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.

Lean proof agents

Open PDF Semantic Scholar

core score 6.5 2026-07-10 arXiv

Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing

Seongmin Lee, Yaoxuan Wu, Miryung Kim

As the cost of code generation becomes cheaper with AI, the new bottleneck in software engineering has shifted to intent specification and validation. Overcoming this durability crisis of AI-driven coding requires more than traditional fuzzing: each candida...

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

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

adjacent score 4.9 2026-07-12 arXiv

The Prime Digit Distribution Conjecture: A Formal Proof of Average Digit Equidistribution in the Prime Numbers

Mahadee Al Mobin, Md. Shariful Islam

Let $S_n=\{p\in\mathbb{P}:p<10^n\}$, $N_n$ denote the total number of decimal digits occurring in the primes of $S_n$, $C_n(d)$ be the number of occurrences of a digit $d\in\{0,\ldots,9\}$ among those digits, and $P_n(d)$ be the probability of occurrence of...

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.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-07-09 arXiv

Minimum modulus for the unique multiset-sum problem

José A. R. Fonollosa

Fix n >= 2. A set A = {a_0 < a_1 < ... < a_{n-1}} of n residues in Z_N is "valid mod N" if the all-ones multiset is the only size-n multiset drawn from A whose sum is p := sum_i a_i (mod N). For the super-increasing set A = {2^k - 1 : 0 <= k <= n-1} we dete...

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.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-07-09 arXiv

A counterexample to a subadditivity conjecture of Cohen for Sophie Germain cyclic numbers

Josué Alexander Ibarra

An integer $n \ge 1$ is cyclic if $\gcd(n,\varphi(n))=1$ (equivalently, if every group of order $n$ is cyclic), and Sophie Germain cyclic if both $n$ and $2n+1$ are cyclic. Let $C_σ(N)$ count the Sophie Germain cyclic integers in $[1,N]$. Cohen conjectured...

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-07-14 arXiv

Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs

Junyu Ren

Tool access alone does not make LLM empirical reasoning governable: accepted outputs need not descend from attested evidence, and accepted deductions need not hold up under formal scrutiny. We present EG-VAR (Evidence-Grounded Verified Agentic Reasoning), a...

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

An Agentic Formalization for Certified Quantum Neural Network Design

Mingrui Jing, Lei Zhang, Yusheng Zhao et al.

A central model in quantum machine learning is the quantum neural network (QNN), whose design requires balancing expressivity and trainability. Technically, expressivity is studied through circuit-function analysis, such as quantum signal processing, while...

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

System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)

Yichen Xu, Oliver Bračevac, Cao Nguyen Pham et al.

Substructural type systems give strong static control over aliasing. Examples include uniqueness, separation, and borrowing. How can such control be brought to established languages whose programming models rely on higher-order abstraction, unrestricted ali...

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

New bounds for double covers of the discrete box {0,1,2}^d

Patrick White

A proper sub-box of $A=\{0,1,2\}^d$ is a product $S_1\times\dots\times S_d$ with each $\varnothing\neq S_i\subsetneq\{0,1,2\}$. A double cover is a finite multiset of proper sub-boxes covering every point of $A$ exactly twice; write $f(d)$ for the minimum s...

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

A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game

Joseph K. Miller

We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game. The objective is to turn a LaTeX document into Lean. The game is won when the development compiles, c...

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

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

negative score 0.8 2026-07-15 GitHub

leanprover/lean4: perf: use WHNF cache in `whnfMatcher` also at sub-default transparency (#14323)

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

leanprover/lean4: perf: optimize `String.charactersIn` (#14395)

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

leanprover/lean4: fix: show correct tactic state in whitespace between tactics without incrementality (#14396)

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

leanprover/lean4: fix: make String.toList semireducible (#14294)

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

leanprover/lean4: feat: store traces in memory for deeper inspection (`store_traces_as`) (#14386)

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

leanprover/lean4: feat: persist `logLintExt` data at `server` level (#14387)

Wojciech Różowski

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

leanprover/lean4: feat: make tactic `set_option` incremental (#14397)

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

leanprover/lean4: feat: grind propagators that evaluate BitVec operations on literals (#14393)

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

Source Health

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

None