AI4Math

4core

13adjacent

73downweighted

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

Source Mix

arXiv17

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

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

Watch Later

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

adjacent score 3.5 2026-08-18 arXiv

Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits

Olga Mashkova, Asaad Mohammedsaleh, Fernando Zhapa-Camacho et al.

OWL 2 DL ontologies, grounded in the description logic $\mathcal{SROIQ}$, express large knowledge bases in biomedicine and the Semantic Web. Neuro-symbolic (NeSy) learners over description logics either embed the ontology in a continuous space, abandoning c...

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

Graph Surgery and the Do-Operator: A Precise Correspondence for Acyclic Structural Causal Models

Satpreet Makhija

The $\operatorname{do}$-operator is described graphically by deleting arrows into its targets and functionally by replacing their mechanisms with constants. To call these operations equivalent is not yet a mathematical statement: one returns a graph and rem...

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

adjacent score 1.9 2026-08-18 arXiv

An equidistribution conjecture for quotient-closed and submodule-closed subcategories

Haruhisa Enomoto

We study subcategories of the module category of a finite-dimensional algebra that are closed under quotients or submodules. We propose the quotient--submodule equidistribution conjecture: over a representation-finite algebra, the number of quotient-closed...

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

negative score 0.8 2026-08-25 GitHub

leanprover/lean4: refactor: make `UIntX.ofNatClamped` use `BitVec.ofNatClamped` (#14917)

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

leanprover/lean4: fix: skip data-valued constructions for small-eliminating inductives (#14909)

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

leanprover/lean4: fix: enforce set notation per-element indentation (#14350)

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

leanprover/lean4: fix: do not register the well-founded recursion simprocs globally (#14922)

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

leanprover/lean4: fix: do not apply simproc candidates selected for a rewritten expression (#14921)

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

leanprover/lean4: fix: correct lean_kernel_diag_is_enabled declaration to match generated C (#14886)

Fawad Haider

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

leanprover/lean4: fix: correct LEAN_EXPORT attribute order in ffi.cpp (#14888)

Joe Hendrix

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

leanprover/lean4: feat: add strong (co)induction principles for lattice-theoretic predicates (#14855)

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

Source Health

Warnings are preserved so failed sources do not silently disappear from the brief.

None