Daily field radar

AI4Math Radar

Start with VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving, then A Semantic Search Engine for Mathlib4. 9 useful item(s) are recent enough to scan today.

2026-06-20
Latest Newer Older
America/Los_Angeles Generated 2026-06-20T15:36:58Z JSON data
11core
14adjacent
69downweighted
0warnings

Today's Scan

Start with VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving, then A Semantic Search Engine for Mathlib4. 9 useful item(s) are recent enough to scan today.

Source Mix

  • arXiv19
  • Semantic Scholar3
  • Scholar Inbox2
  • X1

Best Use

Open only the first lane during a busy morning. Use the queue buttons to keep a local reading list for the day.

Start Here

The top few items most likely to matter for formal proof agents or Lean-facing AI4Math work.

1
core score 12.5 2026-06-17 arXiv

VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

Manish Acharya, Zhenyu Liao, Yueke Zhang et al.

LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit. We present VERITAS, a zero-shot framework that routes every verifier signal back into proof search through a t...

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
2
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
3
core score 9.0 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

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

Process-Verified Reinforcement Learning for Theorem Proving via Lean

Minsu Kim, Se-Young Yun

While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This gap between structured processes and un...

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.

RL or distillationverifier feedback
Open PDF Semantic Scholar
5
core score 7.9 2026-06-14 arXiv

Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning

Ji Feng, Zhouxing Shi

With large language models (LLMs) increasingly applied to mathematical reasoning, formal proof assistants such as Lean can be leveraged to verify reasoning outputs with machine-checkable rigor, enabling use cases such as answer selection in test-time scalin...

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

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 reasoningLean proof agents
Open PDF Semantic Scholar
6
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
7
core score 6.5 2026-06-17 arXiv

DeFAb: A Verifiable Benchmark for Defeasible Abduction in Foundation Models

Patrick Cooper, Alvaro Velasquez

A rule-based logic solver resolves every instance in our benchmark in under 50 microseconds with 100% accuracy; the best frontier language model reaches 65% at best and drops to 23.5% under rendering-robust evaluation (worst case over four surface rendering...

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
core score 6.5 2026-06-15 arXiv

Formalizing chip-firing and Riemann--Roch for graphs in Lean 4

Dhyey Dharmendrakumar Mavani, Nathan Pflueger

The Riemann--Roch theorem for graphs, due to Baker and Norine, is a foundational result establishing a powerful analogy between finite graphs and algebraic curves. We describe a complete formal proof of this theorem implemented in the Lean 4 theorem prover....

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
9
core score 6.5 2026-06-15 arXiv

The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements

Noor Islam S. Mohammad, Tamim Sheikh

Autoformalization, translating natural-language mathematics into formal proof assistants, is bottlenecked not by translation fluency but by \emph{faithfulness}: a formal statement can typecheck and be provable, yet still encode a different theorem than 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 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.

autoformalizationLean proof agents
Open PDF Semantic Scholar
10
core score 6.5 2026-06-15 arXiv

EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research

Xiaohui Bei, Jiajun Ma, Zhan Jing et al.

Mathematical formalization uses interactive theorem provers to turn informal mathematical statements into machine-checkable artifacts. The success of mathlib, a large collaborative library for Lean, illustrates the potential of this approach. Recent progres...

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.

Lean proof agentsmathlib search
Open PDF Semantic Scholar
11
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
12
adjacent score 4.9 2026-06-17 arXiv

Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation

Ruida Wang, Rui Pan, Pengcheng Wang et al.

Enhancing the formal math reasoning capabilities of Large Language Models (LLMs) has become a key focus in both mathematical and computer science communities in recent years. While significant progress has been made in using state-of-the-art Auto-Regressive...

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.

AI math reasoningLean 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 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
14
adjacent score 3.5 2026-06-18 arXiv

Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4

Fubin Yan, Kenneth W. Shum

The extended complex plane is a fundamental object in complex analysis, hyperbolic geometry, and mathematical physics. Its geometry is governed by Möbius transformations, with the cross ratio serving as a central invariant. We present a formalization of the...

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
15
adjacent score 3.5 2026-06-18 arXiv

BARReL: a modern backend for Atelier B in Lean

Ghilain Bergeron, Vincent Trélat

BARReL is a Lean 4 library bridging Atelier B, an industrial tool for the B method, and the Lean proof assistant by enabling users to conduct their formal B developments -- up to machine refinement and implementation -- interactively inside Lean, while reta...

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
16
adjacent score 3.5 2026-06-18 arXiv

Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4

Leni Aniva, Claire Wang

Music theory obeys a rich set of mathematical rules and symmetries. These symmetries follow mathematical structure which can be verified and expressioned in the precise language of a proof assistant. In this paper, we present Prismriver, a formalization of...

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
17
adjacent score 3.5 2026-06-18 arXiv

Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic $L(\forall)$

Lars Warren Ericson

We present a machine-checked completeness theorem, in Lean 4, for the hybrid logic $L(\forall)$: propositional modal logic with nominals, the satisfaction-style binder $\forall$, and the box modality. (Machine-checked completeness for basic hybrid logic, wi...

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

Exact 6-cut rigidity and small-order superconnectivity for the 6-regular case of Dirac's k=4 problem

Alper Ferudun

Dirac asked in 1970 whether for every k >= 4 there is a k-vertex-critical graph without critical edges; Jensen settled all k >= 5, and only k=4 remains open. Following Skottova and Steiner, call a graph G a (4,1)-graph if chi(G)=4, chi(G-v)=3 for every vert...

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
Downweighted 69 low-priority match(es), folded for daily reading.
1
negative score 0.8 2026-06-20 GitHub

leanprover/lean4: chore: CI: fix `macos-arm-ci` label spelling in restart-on-label (#14132)

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-06-20 GitHub

leanprover/lean4: test: reuse snapshots of most common headers across elab pile (#14077)

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

leanprover/lean4: fix: lake: correct `Package.remoteUrl?` logic (#14130)

leiko

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
4
negative score 0.8 2026-06-20 GitHub

leanprover-community/mathlib4: chore(FieldTheory/IntermediateField/Basic): automated extraction from #38864 (#40844)

mathlib-splicebot[bot]

Recent commit on leanprover-community/mathlib4.

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

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-06-20 GitHub

leanprover-community/mathlib4: chore(Algebra/Group/Subgroup/Basic): automated extraction from #38864 (#40842)

mathlib-splicebot[bot]

Recent commit on leanprover-community/mathlib4.

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

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-06-20 GitHub

leanprover-community/mathlib4: refactor(RingTheory/Localization/FractionRing): remove bottom ring and field from `IsFractionRing.mulSemiringAction` (#40804)

Thomas Browning

Recent commit on leanprover-community/mathlib4.

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

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-06-20 GitHub

leanprover-community/mathlib4: chore(RingTheory/Polynomial/Basic): squeeze terminal `simp`s (#40833)

Yi.Yuan

Recent commit on leanprover-community/mathlib4.

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

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-06-20 GitHub

leanprover-community/mathlib4: doc(1000-yaml): we don't have Cauchy's integral theorem (#40335)

Snir Broshi

Recent commit on leanprover-community/mathlib4.

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

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.