Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.35596

KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents

Zihua She·Xiao Wang
View original source ↗Read source document ↗Export metadata ↓

Abstract

Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organizes language model agents, run by Claude Code, to translate the proofs of a LaTeX paper into the proof assistant Lean 4 with its library Mathlib and check them there, result by result. Each numbered result receives one of four verdicts: verified unconditionally; verified conditionally, with every cited or unproved input stated as a named hypothesis; issue recorded, with its place in the paper and the side at fault; or unfinished, with the reason. The kit follows the paper's own proof step by step, rather than finding a new one. Separate agents write and review, each statement is compared with the paper before it is proved and fingerprinted afterwards, and every verdict rests on evidence that can be rerun without a language model. The kit runs unattended for hours, waits out usage limits, re-checks only what a revision changed and reports its cost by role, model and result. We describe the design, walk through a complete run, and apply the kit to four example papers with answer keys and to three published statistical papers, checked blind in their versions from before public corrections. In all three, the kit found the published error at the step that the correction names, together with further problems that we confirmed by hand. Given the same papers directly, the same language model working with Lean classified fewer results correctly on the longest paper and reported some statements narrower than the paper's as proved; no verdict of the kit claimed more than its Lean evidence showed.

Explore related subjects

stat.COcs.AIcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Zihua She, Xiao Wang. 2026-10-26. KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents. https://arxiv.org/abs/2610.35596

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A new gradient-free active subspace estimation method with application to rare event probability estimation

To reduce the cost of estimating the probability of a rare event involving a very large number of random parameters, we propose a new strategy for dimension reduction coupled with a surrogate model for the expensive part of the algorithm. To this end, we extend the Ordinary Kriging Active Subspace (OK-AS) method into a sequential version. Our approach consists of iteratively re-estimating the active subspace using a Kriging surrogate trained in a rotated coordinate system until the active subspace stabilises. This method allows for a reduction in prediction error and a better approximation of the active subspace on a benchmark of test problems. Furthermore, we integrate our algorithm into an efficient pre-existing approach for estimating the probability of a rare event. This approach is based on learning the active subspace associated with the random event whose probability is to be estimated. The sequential learning of an importance sampling density is necessary and corresponds to the expensive part of this strategy. To circumvent this issue, we integrate our sequential OK-AS version into the estimation of the importance sampling density. The numerical results indicate that our method allows for reducing the cost required to obtain a precise estimate of the rare event probability.

stat.CO↗
arXiv2026

QuantileMix: A Python package for quantile g-computation

Health researchers often study how a mixture of pollutants or nutrients relates to health. Quantile g-computation addresses this question by giving each exposure an ordered score and fitting a model for the outcome. For example, dividing an exposure into four quantile groups gives scores 0, 1, 2, and 3. The model can compare score 1 with score 2 for every exposure at once. These groups need not contain equal numbers of observations when measurements are tied. A one-score increase can represent different changes in the original units for different exposures. QuantileMix provides selected quantile g-computation methods in Python. It returns estimates, confidence intervals, predictions, and diagnostics for continuous, binary, count, and survival outcomes. Other models handle measurement limits, outcomes with several categories, and counts with many zeros. Fitting and prediction use NumPy and SciPy and do not require R. The package includes a reference manual, runnable examples, and numerical comparisons with R.

stat.CO↗
arXiv2026

Analytically Optimal Sample Allocations for Nested Multivariate Multifidelity Control Variate Estimators

Monte Carlo estimation, an essential tool for quantifying uncertainty in complex scientific and engineering applications, often has unacceptably large errors when computing resources are limited and each sample requires evaluating an expensive high-fidelity model. Multifidelity control variate methods seek to increase the accuracy of Monte Carlo estimation by combining a limited number of expensive high-fidelity samples with a larger number of cheaper lower-fidelity samples. Many different multifidelity estimators have been proposed, including multilevel Monte Carlo (MLMC), multifidelity Monte Carlo (MFMC), approximate control variates (ACVs), and multilevel best linear unbiased estimators (MLBLUEs). An important design choice in multifidelity estimation is the allocation of a limited computational budget among the available models to minimize estimator error. The state of the art in solving this budget allocation problem relies on numerical optimization; to date, closed form solutions have only been derived for estimator forms known to be suboptimal. In this work, we provide closed form expressions for optimal fractional sample allocations for a large class of nested multifidelity control variate estimators, in which higher-fidelity models are evaluated on a subset of the inputs that lower-fidelity models are evaluated on. Our analysis is based on reformulating nested MLBLUEs as an extended version of the MFMC estimator, and is applicable to general multivariate Monte Carlo estimation. We additionally propose a new approach for integer-valued budget allocation based on a greedy strategy used in combinatorial optimization, as well as a method for robust approximation of control variate coefficients from limited pilot samples. Two numerical examples illustrate our theoretical results and demonstrate the increased accuracy of our extended MFMC formulation relative to existing estimators.

stat.CO↗