Papers With

← All papers
First page of Proof Perplexity: A Probabilistic Approach to Measuring non-triviality in Machine Generated Proofs

Proof Perplexity: A Probabilistic Approach to Measuring non-triviality in Machine Generated Proofs

Madhuparna Das, Soumya Banerjee

math.LO Oct 15, 2026 · v1
benchmark mathlib theorem-proving-ml number-theory
Read PDF arXiv abstract
TL;DR
Defines a proof-perplexity metric over Lean kernel declaration dependency trees relative to Mathlib, applied to a Lean 4 formalized Riemann zeta proof.
Abstract
In this article, we propose a benchmark to quantify the non-triviality and novelty of machine-generated mathematical proofs compared to existing literature. Our core methodology uses a probabilistic measure to evaluate the non-triviality of the underlying mathematical arguments in comparison to the current MATHLIB library. Finally, we apply this benchmark to the recent proof generated by Claude on the complex zeros of the Riemann zeta function to test for non-trivial steps.
Problem

It is hard to measure whether a machine-generated proof is a genuinely novel, non-trivial argument or a recombination of results already in the literature.

Approach

Proof steps are modeled as Lean declarations whose kernel-checked dependency closures within Mathlib form a DAG, which is unfolded into internal complexity trees. Each step receives a recoverability score from two parts: ablation recoverability, based on regenerating the step under a search budget, and a Mahalanobis-distance outlier p-value against clusters of Mathlib declarations. These scores give per-step surprisal, a weighted proof perplexity, and a theta-invention fraction with a provable lower bound.

Results

Applied to Claude's Lean 4 formalized proof on zeros of the Riemann zeta function, the method gives a proof perplexity of 388.23 (cap 501). The theta-invention fraction is 0.9578, which satisfies the derived bound of 0.9446, and 2032 of 2399 steps fall at or below the threshold.

MetricValue
Proof perplexity PP_w(π,B)388.23 (cap: 501)
θ-invention fraction β(θ,B)0.9578 (bound: 0.9446, holds)
Steps with α ≤ θ / total2032 / 2399
Proof perplexity results for Claude's Riemann zeta proof