Daily field radar

AI4Math Radar

Start with MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4, then Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair. 11 fresh useful item(s) are inside the 21-day content window.

2026-08-04
Latest Newer Older
America/Los_Angeles Generated 2026-08-04T17:13:56Z JSON data
2core
9adjacent
78downweighted
0warnings

Today's Scan

Start with MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4, then Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair. 11 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv11

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.3 2026-08-03 arXiv

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

Hao Shen, Junyu Guo, Tian Cui et al.

We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically trans...

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

autoformalizationAI math reasoningLean proof agentstool-use agents
Open PDF Semantic Scholar
2
core score 6.5 2026-07-30 arXiv

Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

Ha Trung Tran

Verification consumes the majority of modern chip design effort, yet the formal verification tools that provide mathematical guarantees of correctness remain expensive and restrictively licensed. While large language models (LLMs) have shown promise for har...

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
3
adjacent score 4.9 2026-08-03 arXiv

LEAP: Lean Environment-Feedback via Adaptive Pruning for Code RL in GPU Kernel Generation

Tankun Li, Zhi Chen, Yaohua Tang

Post-training large language models (LLMs) via reinforcement learning (RL) has significantly advanced code generation capabilities. To bypass the heavy memory footprint of critic networks, current state-of-the-art frameworks leverage critic-free paradigms l...

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

Worth Opening

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

4
adjacent score 3.5 2026-08-02 arXiv

Three Graffiti.pc Conjectures on Largest Induced Trees: Proofs of Conjectures 141, 142, and 143

Alper Ferudun

For a finite simple graph $G$, let $t(G)$ be the largest order of an induced tree and let $g(G)$ be the girth. We prove three consecutive conjectures of DeLaViña's Graffiti.pc program. First, writing $\ell(v)$ for the independence number of the subgraph ind...

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
5
adjacent score 3.5 2026-07-31 arXiv

The $δ$-calculus: from distinction to arithmetic

Jonathan Washburn, Milan Zlatanović

Let $δ$ denote the primitive act of distinction, formally realized as the one-step extension $r \mapsto Sr$ of a finite record. We study the inductively generated $δ$-orbit and its first-order arithmetic presentation $\mathbb{N}_δ$. The corresponding $δ$-ca...

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
6
adjacent score 3.5 2026-07-30 arXiv

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

Ruslan Khrulev

LLM-based Lean proving systems increasingly organize a proof as a blueprint: a dependency graph of formal statements. We introduce BlueprintRepair, a repair interface that lets a model change this graph through ten schema-checked local operations. An operat...

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
7
adjacent score 1.9 2026-08-02 arXiv

The Set of Correlated Equilibrium Payoffs for a Fixed Information Structure Need Not Be Closed

Michael Greinecker, Patrick Lahr, Christoph Schwerdtfeger

Aumann (1974) showed that an atomless public randomization device makes the feasible- and equilibrium-payoff sets of a game with a fixed information structure convex, and asked whether they are closed. We show that, in every case the question leaves open, t...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

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 reasoning
Open PDF Semantic Scholar
8
adjacent score 1.9 2026-08-01 arXiv

Optimal Trading of Microstructure Mean Reversion

Lucas Rabechini Amaral

At the scale of seconds the observed mid carries a stationary, mean-reverting error around a latent efficient price. We build an order book whose own flow produces that error and solve for the trading rule that maximises the long-run average profit rate net...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

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.

AI math reasoning
Open PDF Semantic Scholar
9
adjacent score 1.9 2026-07-31 arXiv

On a conjecture of Han and Xiong for fractional Gaussian binomial coefficients

Ken Ono

Han and Xiong recently extended the Gaussian binomial coefficient $\genfrac{[}{]}{0pt}{}{r+k}{k}_{q}$ to positive rational $r$ and conjectured that its integer trace, the integer-exponent part of the resulting power series, is coefficientwise largest at $r=...

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.

AI math reasoning
Open PDF Semantic Scholar
10
adjacent score 1.9 2026-07-31 arXiv

A Proof of the Dittert Conjecture in Dimension 4 via an Agent-Guided Exact Sum-of-Squares Certificate

Jinhui Li, Beibei Xiong, Zhengfeng Yang

The Dittert conjecture states that the Dittert functional on nonnegative $n\times n$ matrices whose entries sum to $n$ is uniquely maximized by the uniform matrix. We prove the conjecture in dimension $4$. More precisely, let $K_4$ be the simplex of nonnega...

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.

AI math reasoning
Open PDF Semantic Scholar
11
adjacent score 1.9 2026-07-30 arXiv

FaithEyes: Towards Faithful Tool Use via Multi-Agent Process-Image Verification

Haoqing Wang, Xingrun Xing, Wei Xia et al.

Agentic vision-language models (VLMs), which interleave textual reasoning with explicit tool calls such as cropping and code-based image manipulation, have emerged as a compelling paradigm for reliable and interpretable multimodal reasoning. However, recent...

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.

downweight: vision world modelstool-use agentsverifier feedback
Open PDF Semantic Scholar

Watch Later

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

No watch-later items in this run.

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

leanprover/lean4: refactor: decouple loop state and element universes in `Std.Internal.Do` specs (#14675)

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

leanprover/lean4: fix: try the next `@[spec]` candidate when a spec rule does not apply (#14669)

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

leanprover/lean4: feat: make `bv_decide` available in `sym` mode (#14672)

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
4
negative score 0.8 2026-08-04 GitHub

leanprover-community/mathlib4: feat(SimpleGraph/Walk/Operations): more operations API (#41460)

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

leanprover-community/mathlib4: chore(Topology): state Heine–Borel theorem for metric spaces (#42241)

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

leanprover-community/mathlib4: chore(RingTheory/IsGaloisGroup/Basic): automated extraction from #42430 (#42433)

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

leanprover/lean4: refactor: port bv_decide to SymM (#14215)

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