AI4Math

4core

15adjacent

70downweighted

0warnings

Today's Scan

Start with A deterministic sin^2-type algorithm for complex cubic irrationalities with exact periodicity certificates, then A Lean 4 Verification Report for Subregular Affine Cells and the Level $-1$ Vertex Algebra of Type $D$. 19 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv18
GitHub1

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

A deterministic sin^2-type algorithm for complex cubic irrationalities with exact periodicity certificates

Ludovic Tagnon

Hermite asked in 1848 for a representation of real numbers whose eventual periodicity characterizes cubic irrationals. The totally real case was solved by Karpenkov's $\sin^2$-algorithm; the complex case, signature (1,1), is his Problem 4. We study a determ...

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 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 agentsverifier feedback

Open PDF Semantic Scholar

core score 6.5 2026-08-21 arXiv

A Lean 4 Verification Report for Subregular Affine Cells and the Level $-1$ Vertex Algebra of Type $D$

Sihai Jin

We report a Lean 4 formal verification accompanying the paper "Subregular Affine Cells and the Level -1 Vertex Algebra of Type D" (arXiv:2608.11997). The formalization kernel-checks substantial internal parts of the proof architecture, including the Section...

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 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 agentsverifier feedback

Open PDF Semantic Scholar

core score 6.5 2026-08-20 arXiv

ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib

Shane Caldwell

Formal proofs in Lean 4 that pass the kernel's type checker can nonetheless vary widely in quality. We introduce ProofJudge, an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automati...

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.

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-08-19 arXiv

Grading the Graders: Verification Autonomy Levels (L0-L5) for LLM Reasoning

Yajie Yin

Large language models (LLMs) are increasingly paired with verifiers (step checkers, self-consistency filters, tool-based fact checkers, formal proof assistants) that claim to detect the model's errors. Yet the verification literature uses the word "level" 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 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 agentsverifier feedback

Open PDF Semantic Scholar

adjacent score 4.9 2026-08-19 arXiv

The Equality Cases of the Weak Simplex Conjecture

Mengwei Su, Kaiwen Yang, Hao Xu et al.

Among $n+1$ equiprobable equal-energy signals in $\R^n$ under additive white Gaussian noise with maximum-likelihood decoding, which arrangement maximizes the probability of correct decoding? The question is Shannon's, recorded by Rice in 1950. Mulgund prove...

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-08-25 arXiv

A dual reformulation of the complex sin^2-algorithm: exact identities, descent, and finiteness

Ludovic Tagnon

We develop the structure theory of the deterministic $\sin^2$-type algorithm for complex cubic fields introduced in the companion paper, addressing the complex-signature case of Karpenkov's Problem 4. The selection rule is shown to be, exactly, the minimiza...

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

Relative formalization in Isabelle/HOL of a result in inverse problems

Cătălin I. Cârstea

This reports on an experiment in autoformalization of arxiv:2606.15977, an inverse problems result for piecewise polynomial anisotropic conductivities, using Isabelle/HOL. The proof of the result is relative to a number of external results which were deemed...

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

adjacent score 3.5 2026-08-24 arXiv

Multi-Winner Voting with Argumentative Ballots

Ryuta Arisaka, Hirotaka Ono

We introduce multi-winner voting with argumentative ballots (MVArg) and investigate theoretical properties. As our conceptual contribution, we generalise approval ballots to argumentative ballots, thereby allowing voters to express defeasible preferences ov...

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

Improved bounds for the smallest 4-chromatic graph of girth six

Glauco Rampone

For integers $k,g \ge 3$ let $n_g(k)$ denote the minimum order of a graph with chromatic number $k$ and girth at least $g$. Exoo and Goedgebeur (DMTCS 2019) proved $26 \le n_6(4) \le 66$; their 66-vertex witness has remained the smallest known 4-chromatic g...

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

ATHENA: Knowledge-guided agentic neural architecture search for AutoFormer-based electronic health record modeling

Deyi Li, Qi Xu, Lingyao Li et al.

Transformer-based models are widely used for clinical prediction from electronic health records (EHRs), yet their architectures still require substantial manual tuning, and the optimal configuration may vary across tasks and hospitals. Neural architecture s...

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

verifier feedback

Open PDF Semantic Scholar

adjacent score 3.5 2026-08-21 arXiv

AI with Authority, from Application to Silicon

Jason Hickey

For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI inverts this relationship: at AI speed, machine verification is not only economical but essential to productiv...

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 agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-08-20 arXiv

FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models

Dingzirui Wang, Xuanliang Zhang, Keyan Xu et al.

Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research, yet existing benchmarks remain far from realistic research settings. We introduce \ourbenchmark, an expert-validated benchmark for evaluatin...

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.

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-08-20 arXiv

A Fixed-Penalty Linearized Augmented Lagrangian Method with Classical Multiplier Updates

Benqi Liu, Kangkang Deng, Zichen Wang et al.

Augmented Lagrangian methods are effective for nonlinear equality-constrained optimization, but solving their nonlinear primal subproblems can be expensive. For smooth nonconvex problems with deterministic or stochastic objectives, we propose a nonlinear-re...

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-08-19 arXiv

The Position-wise Prime Digit Distribution Theorem: A Formal Proof of Position-wise Digit Equidistribution in the Prime Numbers

Mahadee Al Mobin, Md. Shariful Islam

We state and prove the Theorem: for primes $p < 10^n$ with base-$10$ expansion $p = \sum_{k=0}^{n(p)-1} d_k(p) 10^k$, the positional digit probabilities $P_n(d \mid k)$ satisfy \[ \lim_{n \to \infty} P_n(d \mid k) = \begin{cases} 1/10, & k \ge 1,\ d \in \{0...

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

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-08-19 arXiv

Budget-First Tariff Recommendation (BFTR): A Complete Algorithmic Framework for Telecom Plan Recommendation without Overcharging

Ghislain Dorian Tchuente Mondjo

Telecom operators traditionally offer predefined tariff grids, forcing users to choose from a limited set of plans. This paper proposes BFTR (Budget-First Tariff Recommendation), a complete algorithmic framework integrating eight Budget-First strategies, in...

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

A Kernel-Checked Exclusion Certificate for Erdős Problem 647

Ibrahim Mian, Shayaan Siddique

Erdős problem 647 asks whether any $n > 24$ satisfies $\max_{m<n}(m + τ(m)) \le n + 2$, where $τ$ is the divisor-count function. Computational searches have excluded solutions up to $10^{12}$ by direct sieve and up to roughly $9.17 \times 10^{18}$ within a...

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.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 2.2 2026-08-25 GitHub

leanprover-community/mathlib4: chore(Archive/Imo): convert to the module system (#42962)

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.

AI math reasoning

Open Semantic Scholar

adjacent score 1.9 2026-08-22 arXiv

The General Subgroup Permanental-Dominance Conjecture in Order Four

Siwei Zeng

The general subgroup permanental-dominance conjecture was previously known only through matrix order three. This paper proves its complete order-four case: for every subgroup $H\leq S_4$, every irreducible complex character $χ$ of $H$, and every $4\times 4$...

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

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

negative score 0.8 2026-08-26 GitHub

leanprover/lean4: refactor: persist code quality entries in an environment extension (#14914)

Wojciech Różowski

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

leanprover/lean4: feat: support some symbolic `Nat` operations in `bv_decide` (#14928)

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

leanprover/lean4: feat: add a `leanchecker-paranoid` binary with mimalloc mitigations (#14884)

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

leanprover-community/mathlib4: refactor: change the default value of `Measure.map` to a Dirac mass (#42322)

Etienne Marion

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

negative score 0.8 2026-08-26 GitHub

leanprover-community/mathlib4: perf(Condensed/Light): speedup kernel typechecking of `InternalProjectivityProof.cocone` (#41703)

Aaron Liu

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

negative score 0.8 2026-08-26 GitHub

leanprover-community/mathlib4: feat(MeasureTheory/Group/Circle): add MeasurableSpace/BorelSpace instances for the circle (#42953)

teorth

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

negative score 0.8 2026-08-26 GitHub

leanprover-community/mathlib4: feat(MeasureTheory): basic lemmas for absolute continuity (#42992)

dean cureton

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

negative score 0.8 2026-08-26 GitHub

leanprover-community/mathlib4: feat(GroupTheory/Presentation): define group presentations (#41936)

Hang Lu Su

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