AI4Math

3core

18adjacent

69downweighted

0warnings

Today's Scan

Start with Formal Model Construction Guided by Model-Based Proof Sketches, then A New Upper Bound for the Turán Density of the Tetrahedron. 21 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv21

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.

core score 6.5 2026-09-24 arXiv

Formal Model Construction Guided by Model-Based Proof Sketches

Hongshu Wang, Xinyue Zuo, Yufan Cai et al.

Formal modeling provides strong guarantees about system correctness, but developing and repairing formal models remains labor-intensive and requires substantial expertise in logic and formal reasoning. Recent LLM-based autoformalization agents seek to reduc...

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.

autoformalizationverifier feedback

Open PDF Semantic Scholar

core score 6.5 2026-09-23 arXiv

A New Upper Bound for the Turán Density of the Tetrahedron

Gyeongwon Jeong, Seonghun Park, Seonghyuk Im et al.

We prove that the Turán density of the tetrahedron $K_4^{(3)}$ satisfies $π(K_4^{(3)}) \le 312372062889819/560000000000000 < 0.557808$, improving Baber's upper bound of $0.5615$ and closing about $62\%$ of the gap to the conjectured value $5/9$. The proof u...

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

core score 6.5 2026-09-22 arXiv

Simple symmetric Venn diagrams with 17 and 19 curves

Chris Dzoba

We exhibit simple, rotationally symmetric Venn diagrams with 17 curves and with 19 curves: n Jordan curves carried to one another by rotation through 2π/n, with every one of the 2^n regions present and connected and, since the diagrams are simple, every cro...

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 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.

adjacent score 4.9 2026-09-23 arXiv

Three Conjectures on Binary Channels for the Doubly Symmetric Binary Source

Georg Pichler

We settle three conjectures concerning a doubly symmetric binary source $(X,Y)$ with crossover $p$. Consider Markov chains $U - X - Y - V$ with $U,V$ binary, and let $\mathcal{A}$ be the set of rate triples $(I(U;V),I(U;X),I(Y;V))$ attainable with arbitrary...

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.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-09-23 arXiv

Learning to Discover Interesting Mathematics

Niket Patel, Ahmad Rammal, Amaury Hayat et al.

Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to expansion of mathematical knowledge at unprecedented scale. Yet, while LLMs ma...

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.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-09-23 arXiv

A Spectral Proof of Khachiyan's Ellipsoid Conjecture

Zhou Longfei, Haijun Zou, Tianhao Liu

For a convex body $K\subset\mathbb{R}^n$, let $w(K)$ denote the volume of its maximum-volume inscribed ellipsoid. We prove that every closed halfspace $H$ whose boundary passes through the center of the maximizing ellipsoid satisfies \[ w(K\cap H)\le\frac{\...

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.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-09-22 arXiv

A weak Hellinger inequality for noisy Boolean channels

Polona Durcik, Marco Fraccaroli, Joris Roos

A weak form of the Hellinger conjecture of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair for the binary symmetric channel is proved: dictator functions maximize Hellinger $Φ$-entropy among all Boolean functions of the input and all one-bit statistics...

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.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-09-24 arXiv

Steelhead: Interleaving Partially Synchronous and Asynchronous Commit Rules on a Shared DAG

George Danezis, Zeno De Angeli, Philipp Jovanovic et al.

Dual-mode consensus protocols are fast when the network is partially synchronous and remain live under asynchrony. We introduce Steelhead, a dual-mode mechanism that composes a partially synchronous and an asynchronous commit rule over one DAG: every k-th r...

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-09-24 arXiv

ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions

Lihan Xie, Zhicheng Hui, Yingjun Lan et al.

Existing formal mathematics benchmarks, such as miniF2F, ProofNet, and PutnamBench, primarily evaluate models on constructing complete formal proofs for challenging problems. Because success is measured at the theorem level, these benchmarks offer limited i...

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

adjacent score 3.5 2026-09-23 arXiv

Phase retrieval from a uniformly discrete point set

Jaume de Dios Pont, Josef Greilhuber, Lukas Liehr et al.

We prove that for every window $w$ of the form $w(x) = e^{-π|x|^2} h(x)$, where $h$ is a polynomial, there exists a uniformly discrete set of points $\mathcal{S} \subset \mathbb R^{2d}$ such that the magnitude of the short-time Fourier transform $V_w f$ on...

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-09-23 arXiv

Packing Tails of Reciprocal Rectangles into Squares of Equal Area

Yu Jiang

The Meir--Moser rectangle-packing problem asks whether all rectangles with side lengths $1/n$ and $1/(n+1)$, for $n\ge1$, can be packed into the unit square with pairwise disjoint interiors. We establish a tail version of this problem. Let $R_n$ den...

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-09-23 arXiv

Biplanar graphs with independence number two are 9-colorable

Stefan Szeider

A graph is biplanar if it is the union of two planar graphs on the same vertex set. The largest chromatic number of a biplanar graph is known to lie between 9 and 12. The lower bound comes from Sulanke's graph, which has independence number 2, and a biplana...

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

Watch Later

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

adjacent score 3.5 2026-09-22 arXiv

Provably Complete Generalized Planning with LLMs

Katharina Stein, Chaahat Jain, Jörg Hoffmann et al.

Generalized planning aims to compute a plan that solves all instances of a planning domain. Recent work has used LLMs to automatically generate and debug such generalized plans in the form of Python programs and achieved perfect test data coverage for sever...

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

adjacent score 3.5 2026-09-22 arXiv

Hydrozoan: Latency-Adaptive DAG Consensus under Mixed Byzantine and Crash Faults

Qianyu Yu, Lefteris Kokoris-Kogias, Alberto Sonnino

DAG-based consensus protocols can achieve great throughput and the optimal three-message-delay limit for n = 3f+1 consensus. While two-delay protocols exist, they pay with reduced resilience (requiring 5f+1-style committees) or rely on fallbacks that sacrif...

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-09-22 arXiv

Direct Optimization of Generators for Search in Automated Theorem Proving

Adam Ousherovitch, Ambuj Tewari

Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt generation. Recent work shows cross entropy is suboptimal for an LLM...

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

adjacent score 3.5 2026-09-21 arXiv

Universal Fractal Natural Language Decision Map: Real-Time Edge Triage Across Heterogeneous Domains

Volkan Dağlı, Zerrin Dağlı, Dağhan Dağlı

Deploying Large Language Models for runtime operational triage incurs prohibitive latency (>100-500 ms), high VRAM requirements (>4-8 GB), and excessive energy dissipation. Extending Mandelbrot Fractal Neural Synthesis (Dagli et al., 2026), this paper prese...

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-09-21 arXiv

Beyond Natural Language: An Agent-Native Language for Autonomous Science

Yifeng He, Jiachen Liu

As autonomous AI agents take on every stage of scientific inquiry, research output is expanding far beyond human review capacity. Yet scientific communication still relies on natural-language prose: an informal medium prone to ambiguity, hidden assumptions,...

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

Lean proof agents

Open PDF Semantic Scholar

adjacent score 2.9 2026-09-23 arXiv

Constructing Rational Curves via Jets on Projective Varieties with Non-Nef Canonical Bundle

Bin Dong, Guoxiong Gao, Bin Guo et al.

We give an algebraic proof in characteristic zero of the Miyaoka--Mori criterion: every point of a curve of negative canonical degree on a smooth projective variety lies on a rational curve. Our jet technique gives, in addition, an effective numerical decom...

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.

seed author: Bin Dongseed author: Guoxiong Gao

Open PDF Semantic Scholar

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 69 low-priority match(es), folded for daily reading.

negative score 0.8 2026-09-25 GitHub

leanprover/lean4: test: avoid order-dependent `grind` call in `cbv_system_f` (#15314)

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-09-25 GitHub

leanprover/lean4: perf: derive `partial_fixpoint` unfold theorems from a shared fixpoint equation (#15313)

Joachim Breitner

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-09-25 GitHub

leanprover/lean4: fix: cache type class resolution results based on options values they used (#15325)

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-09-25 GitHub

leanprover/lean4: fix: allow nested Verso metadata blocks (#15324)

Emilio Jesús Gallego Arias

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-09-25 GitHub

leanprover/lean4: feat: record option dependencies during typeclass synthesis (#15278)

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-09-25 GitHub

leanprover/lean4: feat: add wf_preprocess theorems for List.any (#11386)

Jason

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-09-25 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-09-25 GitHub

leanprover-community/mathlib4: fix(scripts/autolabel): do not fail CI-step (#43998)

Jon Eugster

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