Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.25357

Studying proof data with proof theory: the case of AI-generated mathematics

Safal Raman Aryal
View original source ↗Read source document ↗Export metadata ↓

Abstract

I present a method for analyzing large collections of formally verified mathematical proofs (e.g. OpenAI's) grounded in some historical and philosophical musings on mathematics in the age of AI. Many of the quantities involved, such as the size of a proof term or the number of redundant steps, are already computed by work on improving automated provers, where they serve as targets. My aim is to turn them into measurements of proofs themselves: compared against a reference library and against each proof's own cut-free form, checked against theorems they must obey, and controlled for how the proofs were compiled. With these instruments, I measure how (much) machine-generated mathematics diverges from human mathematics, and find that AI-written formal proofs realize far less of the logical compression available to them than human mathematicians do (31% against 73% in mathlib, and 55% against 86% on proofs that call no automation). These figures are broadly in line with reports from those who build provers and proof-improvement tools that AI-written proofs are often longer than they need to be.

Explore related subjects

math.LOcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Safal Raman Aryal. 2026-10-18. Studying proof data with proof theory: the case of AI-generated mathematics. https://arxiv.org/abs/2610.25357

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

KEEP EXPLORING

Related papers

arXiv2026

Finite Combinatorics and Fragments of Arithmetic

In fragments of first order arithmetic, definable maps on finite domains could behave very differently from finite maps. Here combinatorial properties of $Σ_{n+1}$-definable maps on finite domains are compared in the absence of $BΣ_{n+1}$. It is shown that $\mathrm{GPHP}(Σ_{n+1})$ (the $Σ_{n+1}$-instance of Kaye's General Pigeonhole Principle) lies strictly between $\mathrm{CARD}(Σ_{n+1})$ and $\mathrm{WPHP}(Σ_{n+1})$ (Weak Pigeonhole Principle for $Σ_{n+1}$-maps), and also that $\mathrm{FRT}(Σ_{n+1})$ (Finite Ramsey's Theorem for $Σ_{n+1}$-maps) does not imply $\mathrm{WPHP}(Σ_{n+1})$.

math.LO↗
arXiv2026

Computational techniques for sheaf cohomology of locally profinite sets

We compute the sheaf cohomology with constant $\mathbb{Z}_2$ coefficients of a concrete class of locally profinite sets of independent interest. We introduce $k$-sheer partitions to aid in constructions. It is also shown that questions of intermediate cohomology degrees can be reduced to questions about top cohomology degrees by exhibiting nontrivial top cocycles as pointwise limits of coboundaries.

math.LO↗
arXiv2026

Computable Quantification in Reflective Grounded Arithmetic

Informal statements of Gödel's incompleteness theorems often run: "any consistent formal system with arithmetic has true but unprovable statements." That reading assumes a classical notion of truth, under which a universal statement is true as soon as each of its numeral instances is. This paper presents reflective grounded arithmetic (RGA), in which truth is grounded in computation and universal quantification is grounded reflectively: a universal statement is true when the system's own proof search certifies its schematic instance, and false when the system refutes one numeral instance. RGA allows recursive definitions without restriction and proves addition, multiplication and Ackermann's function total as theorems quantified inside the system. RGA is consistent, and it is complete for its own, grounded notion of truth: every well-formed statement that evaluates to true is provable. Gödel's theorems still hold for RGA, as a companion paper shows. The statements that classical reasoning calls true but unprovable have every numeral instance provable but no certified schematic instance, so they are ungrounded in RGA; read instance by instance, in an $ω$-semantics for which RGA is also sound, they are true. All results are machine-checked in Isabelle/HOL: soundness and consistency; completeness for grounded truth, open statements included; $ω$-soundness and $ω$-consistency; that grounded truth is recursively enumerable and RGA represents exactly the recursively enumerable sets; and $ω$-incompleteness. The logic is neither classical nor intuitionistic: double negation is eliminable as an entailment, excluded middle fails wherever a statement has no boolean value, RGA has the disjunction and witness properties, and the deduction theorem holds exactly at provably decided hypotheses.

math.LO↗