AI4Math

4core

12adjacent

56downweighted

0warnings

Today's Scan

Start with VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving, then Process-Verified Reinforcement Learning for Theorem Proving via Lean. 9 useful item(s) are recent enough to scan today.

Source Mix

arXiv16

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.

core score 9.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 agentsdownweight: unrelated coding agentsverifier feedback

Open PDF Semantic Scholar

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

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

Worth Opening

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

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

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

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

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

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

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

adjacent score 3.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 Save for later unless the title matches your current proof-agent work.

Lean proof agentsdownweight: unrelated coding agentsverifier feedback

Open PDF Semantic Scholar

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

adjacent score 3.5 2026-06-15 arXiv

Symbolic Informalization: Fluent, Productive, Multilingual

Aarne Ranta

Symbolic informalization enables a reliable conversion of formal mathematics to natural language. It has the potential to make machine-checked content human-readable without loss of precision. In a traditional proof system usage, symbolic informalization ge...

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

Watch Later

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

adjacent score 3.5 2026-06-15 arXiv

A Lean-Certified Proof of $K_8(4, 2) = 23$

Andreas Florath

We prove the exact octonary covering-code value $K_8(4, 2) = 23$ in Lean 4. The upper bound is given by an explicit 23-word radius-two code in $(Fin\:8)^4$ , checked over all $8^4$ ambient words. The lower bound excludes covers with at most 22 words. A fibe...

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

adjacent score 3.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 Save for later unless the title matches your current proof-agent work.

autoformalizationLean proof agentsdownweight: unrelated coding agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-06-15 arXiv

Moment-Free Kunchenko Stochastic Polynomials via Empirical Characteristic Function

Serhii Zabolotnii

We give a characteristic-function formulation of Kunchenko's stochastic-polynomial construction for settings in which raw moments may fail to exist. In the finite-variance trigonometric case, the coefficients of the Kunchenko normal system are expressed thr...

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

adjacent score 3.5 2026-06-15 arXiv

Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization

Lars Warren Ericson

We describe a Lean~4 formalization revisiting NYU Courant Technical Report TR1995-711 on the average-case complexity of Multilevel Syllogistic (MLS). The development encodes Reischuk--Schindelhauer average-case classes, an axiomatic MLS/EMLS semantics layer...

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

Downweighted 56 low-priority match(es), folded for daily reading.

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: fix: `lean_task_imp.m_canceled` needs to be accessed using atomics (#14127)

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

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: chore: update stage0

Lean stage0 autoupdater

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

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: fix: avoid compiler panic when deriving computable `Inhabited` in a `noncomputable section` (#14125)

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

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: feat: split `implicit` transparency into `implicit` and `instances` (#13637)

Kim Morrison

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

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: chore: update release scripts (#14126)

Garmelon

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

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: perf: replace the object compactor's worklist with recursion (#14122)

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

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: feat: extract `WP` superclass from `WPMonad` to support deep embeddings (#14080)

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

negative score 0.8 2026-06-19 GitHub

leanprover/lean4: chore: skip fetching blobs in the "push tag" step of the PR release (#14123)

Paul Reichert

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