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. 10 fresh useful item(s) are inside the 21-day content window.

2026-08-05
Latest Newer Older
America/Los_Angeles Generated 2026-08-05T17:04:19Z JSON data
2core
8adjacent
79downweighted
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. 10 fresh useful item(s) are inside the 21-day content window.

Source Mix

  • arXiv10

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

Screenshots or Tools? Eliciting Tool Use and Managing Multimodal Context in Hybrid GUI-MCP Computer-Use Agents

Siqi Fan, Minghao Li, Xiaoqian Ma et al.

Hybrid computer-use agents can act through screenshots or call text tools. We find that having a tool available does not settle which way the effect goes. Under one identical GUI-MCP harness on the OSWorld-MCP benchmark (309 tasks), the same MCP tools impro...

Why it matters Training signal: worth scanning for reward design, experience collection, or process supervision that could transfer to theorem proving.

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.

RL or distillationtool-use agents
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

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

leanprover/lean4: test: stack with an allocator in the vcgen separation logic demo (#14685)

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

leanprover/lean4: test: in-place append with a ramified spec in the vcgen separation logic demo (#14614)

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

leanprover/lean4: feat: support a destructuring binder on a `for … invariant` loop (#14682)

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

leanprover/lean4: feat: make `bv_decide`'s embedded constraints pass more aggressive (#14683)

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

leanprover-community/mathlib4: refactor(Geometry/Manifold/Instances/Sphere): use mvfderiv when appropriate (#42374)

Michael Rothgang

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.

  • None