Daily field radar

AI4Math Radar

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.

2026-07-07
Latest Newer Older
America/Los_Angeles Generated 2026-07-07T17:33:51Z JSON data
11core
16adjacent
69downweighted
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

  • arXiv21
  • Semantic Scholar3
  • Scholar Inbox2
  • 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.

1
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
2
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
3
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.

4
core score 7.9 2026-07-06 arXiv

FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

Haocheng Wang, Baiyu Huang, Yingjia Wan et al.

The veracious semantic alignment in autoformalization is significant for formal mathematical reasoning. However, existing evaluations provide only opaque binary verdicts or scalar scores, offering no interpretable insight into where or why translations fail...

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.

autoformalizationAI math reasoningverifier feedback
Open PDF Semantic Scholar
5
core score 6.5 2026-07-05 arXiv

LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics

Ján Perháč, Vasyl Khashcha, Samuel Novotný

We present LogicProof, an interactive web-based theorem prover designed for educational use. The system supports natural deduction and sequent calculus for propositional and first-order logic in both classical and constructive variants. It emphasizes a mode...

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.

Lean proof agentsverifier feedback
Open PDF Semantic Scholar
6
core score 6.5 2026-07-04 arXiv

Neuro-Symbolic Reasoning for Vulnerability Detection

Yanjie Zhao, Hongjie Chen, Li Lu et al.

Ask a large language model (LLM) whether a pointer dereference is safe, and it can often produce a plausible justification for ``yes''. The difficulty is that a fluent justification is not a proof. This gap is precisely where automated vulnerability detecti...

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
7
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
8
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
9
adjacent score 3.5 2026-07-05 arXiv

Mechanism-level routing failure in LLMs over Lean-verified algebraic structures

Manuel Israel Cázares, Wenlin Zhang, Haobo Ma

We present an empirical study of structural routing failure in large language models (LLMs) over a formally verified algebraic corpus. The task requires selecting the correct proof-mechanism label from a fixed closed template set for compact mathematical ob...

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
10
adjacent score 3.5 2026-07-03 arXiv

LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean

Simon Jeanteur, Lorenzo Veronese, Magdalena Soltiro et al.

Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-de...

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
11
adjacent score 3.5 2026-07-02 arXiv

Reformalization of the Jordan Curve Theorem

Simon Guilloud, Sankalp Gambhir, Samuel Chassot

We present a case study in reformalization, a variant of autoformalization in which the input proof is not natural language but a formal development in a different proof assistant. Concretely, we report three reformalizations of the Jordan Curve Theorem: fr...

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.

autoformalization
Open PDF Semantic Scholar
12
adjacent score 3.5 2026-07-01 arXiv

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

Michael Saldivar, Ben Slivinski

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

Watch Later

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

13
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
14
adjacent score 3.5 2026-07-01 arXiv

An alternative approach towards attacks against fully-split PLWE instances

Iván Blanco-Chacón, Rodrigo Martín Sánchez-Ledesma, Raúl Durán Díaz

In the present work we address some key questions regarding the generalization of root-based attacks presented in a recent work by the authors. In particular, we analyze potential root-based attacks extensions via the construction of explicit isomorphisms f...

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
15
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
16
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
17
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
18
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

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.

1
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
2
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
3
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
4
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
5
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
6
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 69 low-priority match(es), folded for daily reading.
1
negative score 0.8 2026-07-07 GitHub

leanprover/lean4: test: use plain shareCommon before kernel check in vcgen benchmarks (#14304)

Sebastian Graf

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 the task definition, metric, and whether the benchmark has Lean-checkable artifacts.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar
2
negative score 0.8 2026-07-07 GitHub

leanprover/lean4: perf: `shareCommon` at `SymM` (#14314)

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
3
negative score 0.8 2026-07-07 GitHub

leanprover/lean4: fix: statement of `eqRec_heq_iff` (#13484)

Robin Arnez

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
6
negative score 0.8 2026-07-07 GitHub

leanprover/lean4: feat: bound kernel recursion by `maxRecDepth` (#13956)

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
7
negative score 0.8 2026-07-07 GitHub

leanprover/lean4: chore: remove dead `@[export]` attributes (#14306)

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
8
negative score 0.8 2026-07-07 GitHub

leanprover/lean4: chore: remove custom small allocator (#14149)

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

Source Health

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

  • None