AI4Math

10core

17adjacent

70downweighted

0warnings

Today's Scan

Start with LAMP: Lean-based Agentic framework with MCP and Proof Repair, then A Machine-Verified Proof of a Quantum-Optimization Conjecture. 21 fresh useful item(s) are inside the 21-day content window. 6 older recurring item(s) are parked below.

Source Mix

arXiv20
Semantic Scholar3
Scholar Inbox2
GitHub1
X1

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 13.7 2026-06-27 arXiv

LAMP: Lean-based Agentic framework with MCP and Proof Repair

Santhana Srinivasan R, Maithilee Patawar

Large language models are increasingly capable of mathematical reasoning, but the proofs they generate are often unreliable and hard to verify. Interactive theorem provers such as Lean 4 address this by accepting only kernel-checked proofs; however, their r...

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.

AI math reasoningLean proof agentstool-use agentsverifier feedback

Open PDF Semantic Scholar

core score 10.9 2026-06-29 arXiv

A Machine-Verified Proof of a Quantum-Optimization Conjecture

Uri Kol, Maor Ben-Shahar, Kfir Sulimany et al.

We report a machine-verified resolution of a problem open for over a decade in quantum optimization: the Farhi, Goldstone and Gutmann (FGG) conjecture that depth-$p$ Quantum Approximate Optimization Algorithm (QAOA) on the ring of disagrees attains approxim...

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.

AI math reasoningLean proof agentsmathlib searchverifier feedback

Open PDF Semantic Scholar

core score 9.3 2026-06-30 arXiv

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

Arshia Soltani Moakhar, Iman Gholami, Max Springer et al.

While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly mo...

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.

autoformalizationAI math reasoningLean proof agentstool-use agents

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

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy et al.

Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this setting, compilation is only a validity check: a Lean declaration may type-check...

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

core score 6.5 2026-06-27 arXiv

The Two Genie Game: Adoption and Welfare in Audit-Grounded AI Governance

Darrell Lewis-Sandy

We ask under what conditions an agent with a harm-minimizing policy can displace an approval-seeking (RLHF) agent in a competitive market, and when that policy is sufficient to prevent community harm. We use evolutionary game theory (finite-population Moran...

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

The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization

Chengxiao Dai, Zhaokun Yan, Zhanhui Lin

Headline type-correctness (TC\%) of LLM autoformalization has climbed from $\sim$53\% to $\sim$76\% in two years, yet this scalar conceals which errors each method resolves. We propose a signal-coverage matrix that crosses the Lean elaborator (pass/fail) wi...

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.

autoformalizationverifier feedback

Open PDF Semantic Scholar

adjacent score 4.9 2026-06-30 arXiv

Stabilization Learning: A Paradigm Transition Bridging Control Theory and Machine Learning

Quan Quan

Stabilization learning is an interdisciplinary paradigm that bridges control theory and machine learning. Its core idea is to enable systems to adjust their policies under perturbations or environmental changes through real-time feedback and adaptive mechan...

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 reward construction and whether failures provide dense learning signal.

Read if Save for later unless the title matches your current proof-agent work.

RL or distillationverifier feedback

Open PDF Semantic Scholar

adjacent score 4.9 2026-06-26 arXiv

Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing

Can Li, Ting Zhang, Junbo Zhao et al.

Geometry Problem Solving have increasingly adopt the neuro-symbolic paradigm, combining neural intuition with symbolic rigor. However, current frameworks suffer from severe bottlenecks in two core stages: autoformalization, which treats multimodal translati...

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

Skim cue Skim the reward construction and whether failures provide dense learning signal.

Read if Save for later unless the title matches your current proof-agent work.

autoformalizationRL or distillation

Open PDF Semantic Scholar

adjacent score 3.5 2026-07-01 arXiv

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

Ben Slivinski, Michael Saldivar

When should an AI system's answer be trusted? Formal proof assistants offer certainty but cannot reach most of the problem distribution; scalar LLM judges offer coverage but produce opaque scores that cannot be audited after the fact and are subject to the...

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

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

LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection

Stefan Szeider

SAT solvers settle combinatorial problems beyond the reach of interactive theorem provers and produce LRAT certificates for independent verification. We present LRAT-Catcher, a standalone, general-purpose tool that imports a DIMACS formula together with an...

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

A Priori Integral Persistent Excitation in Conservative Polynomial ODEs with Higher-Order Interactions

Aleksandr Semenov, Alexander Fradkov

The paper proposes an approach for verifying integral persistent excitation, which is important in problems of parameter identification and adaptive control in nonlinear dynamical systems. The approach works for conservative polynomial ODEs a priori without...

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.

verifier feedback

Open PDF Semantic Scholar

adjacent score 3.5 2026-06-29 arXiv

Transformer Architectures as Complete Bayes Processes: A Formal Proof in the Measure-Theoretic Kernel Framework

Haobo Yang

We present a complete formal proof that transformer architectures, when their internal update mechanisms satisfy a Bayes joint-distribution condition, implement exact Bayesian posterior inference. Working within the measure-theoretic kernel framework, we de...

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

Watch Later

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

adjacent score 3.5 2026-06-29 arXiv

A Lean 4 Formalization of Scott's \emph{Continuous Lattices} (1972)

Lars Warren Ericson

We present a complete machine-checked formalization of Dana Scott's landmark 1972 paper \emph{Continuous Lattices} \textbf{[Sco72]}, carried out in Lean 4 against mathlib and including the March 1972 Milner correction in \textbf{[Sco72]} (pp.~135--136). Sco...

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

Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving

Pawan Sasanka Ammanamanchi, Siddharth Bhat, Stella Biderman

Benchmarks for LLM-assisted theorem proving in Lean are often treated as intrinsically reliable because every solved instance comes with a machine-checked proof. However, the kernel only checks that a proof establishes a \emph{formal} statement; it does not...

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 Save for later unless the title matches your current proof-agent work.

verifier feedback

Open PDF Semantic Scholar

adjacent score 3.5 2026-06-28 arXiv

A sharp 5/8 bound for an Erdős-Sós pairwise-sums problem

Ricky Cipollini

Let $f_3(N)$ be the least integer such that every set $A\subseteq\{1,\ldots,N\}$ of size at least $f_3(N)$ contains distinct elements $a,b,c\in A$ such that $a+b\in A$, $a+c\in A$, and $b+c\in A$. We prove that $f_3(N)\le 5N/8+O(1)$. Together with the stand...

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-06-27 arXiv

The Fundamental Theorem of Asset Pricing, Formalized in Lean 4

Raphael Coelho

The Fundamental Theorem of Asset Pricing states that a market is free of arbitrage exactly when it admits an equivalent martingale measure. We formalize it in Lean 4 over Mathlib in three settings: a finite-state market over a finite horizon (Harrison-Plisk...

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

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

Rodrigo Mendoza-Smith

The axiom of choice has divided the foundations of mathematics for over a century, but the distinction between classical and constructive proofs has remained a philosophical and methodological one. We use Lean 4's kernel-level tracking of axiom dependence t...

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-06-25 arXiv

Theory-Scale Auto-Formalization of Logics for Computer Science

Yuming Feng, Frederick Pu, One An et al.

Auto-formalization is critical for scalable formal verification, but existing progress largely focuses on isolated statements, while theory-scale auto-formalization, which coherently translates hundreds of interdependent definitions, lemmas, and theorems, r...

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 Save for later unless the title matches your current proof-agent work.

verifier feedback

Open PDF Semantic Scholar

Older but Useful

6 relevant item(s) are outside the 21-day content window. Keep them for context, but do not let them drive today's scan.

core score 9.5 2025-02-04 Semantic Scholar

A Semantic Search Engine for Mathlib4

Guoxiong Gao, Jiedong Jiang, Haocheng Ju et al.

Semantic Scholar library seed for mathlib retrieval and premise search. This is infrastructure-level signal for theorem-proving agents.

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

mathlib searchseed author: Guoxiong Gaoseed author: Haocheng Juseed author: Jiedong Jiang

Open PDF Semantic Scholar

core score 9.0 observed 2026-06-20 Scholar Inbox

Distilling LLM Feedback for Lean Theorem Proving

unknown authors

Scholar Inbox positive seed for verifier-guided learning from Lean feedback. Useful for proof repair loops and training signal design.

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

verifier feedback

Open Semantic Scholar

core score 7.2 2026-06-08 X

Jui-Hui Chung: Goedel-Architect launch thread

Jui-Hui Chung

X post surfaced during tuning about Goedel-Architect, a Lean 4 formal theorem proving agent built around blueprint generation and refinement.

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 agentsseed author: Jui-Hui Chung

Open Semantic Scholar

core score 6.5 2025-12-19 Semantic Scholar

Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience

Huajian Xin, Zhicheng Jiang, Allan Jie et al.

Semantic Scholar folder seed for experience-driven formal theorem proving. Watch for methods that turn failed proof attempts into useful training data.

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

Lean proof agentsseed author: Allan Jieseed author: Huajian Xinseed author: Zhicheng Jiang

Open PDF Semantic Scholar

adjacent score 4.7 2023-06-27 Scholar Inbox

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Kaiyu Yang, Aidan M. Swope, Alex Gu et al.

Scholar Inbox surfaced this as a core retrieval-augmented Lean theorem proving baseline. It is relevant to premise retrieval, proof search, and agent evaluation.

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

Open PDF Semantic Scholar

adjacent score 3.5 2026-01-20 Semantic Scholar

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Junqi Liu, Marco Dos Santos, Zekai Zhu et al.

Semantic Scholar folder seed for agentic formal mathematics. Relevant to open Lean proof-agent workflows and reusable evaluation setups.

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.

seed author: Junqi Liuseed author: Marco Dos Santosseed author: Zekai Zhu

Open PDF Semantic Scholar

Downweighted 70 low-priority match(es), folded for daily reading.

negative score 0.8 2026-07-02 GitHub

leanprover/lean4: refactor: structure handling in bv_decide (#14241)

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

leanprover/lean4: perf: work around non-linearity in ElimDead (#14245)

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

leanprover/lean4: fix: lake: correct exe perms on restore (#14240)

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

leanprover/lean4: fix: correctly add Verso docstrings to coinductive predicates (#14247)

David Thrane Christiansen

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

leanprover/lean4: doc: fix typo in Quot (#14244)

Julien Cretin

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

leanprover/lean4: chore: shorten pole (#14242)

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

leanprover/lean4: chore: annotate some types (#14250)

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

Source Health

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

None