Daily field radar

AI4Math Radar

Start with Harnessing Code Agents for Automatic Software Verification, then Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics. 23 fresh useful item(s) are inside the 21-day content window. 6 older recurring item(s) are parked below.

2026-07-08
Latest Newer Older
America/Los_Angeles Generated 2026-07-08T16:59:00Z JSON data
10core
19adjacent
68downweighted
0warnings

Today's Scan

Start with Harnessing Code Agents for Automatic Software Verification, then Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics. 23 fresh useful item(s) are inside the 21-day content window. 6 older recurring item(s) are parked below.

Source Mix

  • arXiv23
  • 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 9.5 2026-07-07 arXiv

Harnessing Code Agents for Automatic Software Verification

Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs a...

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

Worth Opening

Good candidates after the first three. These are plausible paper-tab opens, not a mandatory reading list.

4
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
5
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
6
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
7
adjacent score 4.9 2026-07-07 arXiv

SCOPE: Leveraging Subgoal Critiques for Code Generation

Yueke Zhang, Yifan Zhang, Zihan Fang et al.

Code generation with large language models (LLMs) remains unreliable because generated programs can appear correct while still violating key semantic requirements in the natural language specification. Existing feedback-based methods improve over coder-only...

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

Formalizing Scarf, Brouwer, and Nash in Lean

Yuwei Lyu, Kai Li

We formalize in Lean 4 a complete combinatorial route from Scarf's theorem to Brouwer's fixed point theorem and to the existence of mixed Nash equilibria in finite games. The development follows Ivanov's indexed-order formulation of Scarf's theorem, formali...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

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.

Lean proof agents
Open PDF Semantic Scholar
10
adjacent score 3.5 2026-07-07 arXiv

Closed-form fractional radial links for elliptical Mahalanobis discriminant analysis

Serhii Zabolotnii

We study binary classification under shared-generator elliptical class-conditional distributions. The log-likelihood ratio is an additive function of the two squared Mahalanobis radii, with radial link $\varphi=\log g$; QDA is recovered only when this link...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

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.

Lean proof agents
Open PDF Semantic Scholar
11
adjacent score 3.5 2026-07-07 arXiv

Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean

Michael R. Douglas

Mathematicians have embraced interactive theorem provers with growing enthusiasm -- building large shared libraries and machine-checking a string of landmark results. Theoretical physics is different: most of its results are not theorems but justified by ar...

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
12
adjacent score 3.5 2026-07-06 arXiv

Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information

Kazumi Kasaura, Kei Tsukamoto, Kento Mori et al.

Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi relative entropy is a fundamental divergence with various applications, and its data processing inequality (DPI) under quantum channels is a cornerstone result. In...

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

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

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

Simon Jeanteur, Lorenzo Veronese, Magdalena Solitro 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
15
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
16
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
17
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
18
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

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 68 low-priority match(es), folded for daily reading.
1
negative score 0.8 2026-07-08 GitHub

leanprover/lean4: perf: replay tactics when only trailing whitespace is changed (#11958)

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

leanprover/lean4: feat: add Insert instances for NameMap/NameSet (#14153)

Wojciech Nawrocki

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

leanprover/lean4: chore: fix namespaceing in `DeprecatedModule` (#14310)

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

leanprover/lean4: chore: cmake: disable Lake cache on `PREV_STAGE` use as well (#14321)

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

leanprover/lean4: chore: change `UnusedSimpArgs` hint (#14313)

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

leanprover/lean4: chore: CI: re-enable test header snapshots (#14324)

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