Search arXiv⌕ 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

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

Big Ramsey degrees and structures in relational languages

We establish a precompact transfer theorem for big Ramsey structures and a uniform envelope theorem for valuation hypergraphs. These yield big Ramsey structures for generic injective relational structures in languages with finitely many symbols of each positive arity, answering the existence part of Problem~6.3.2 of Balko et al.\ [M.~Balko et al., J.~Eur.~Math.~Soc.\ 28, 2101--2150 (2026)], and refute Conjecture~4.7 of Braunfeld et al.\ [S.~Braunfeld et al., Adv.~Comb., Paper No.~4 (2024)]. We also construct a finitely constrained free amalgamation class in a finite language of maximum arity three whose Fraïssé limit has infinite singleton big Ramsey degree, giving a negative answer to the existence question in Problem~6.3.3 of Balko et al.

math.LO↗
arXiv2026

Hyperwellfoundedness and Eventual Domination

We prove that a Borel strict partial order is an increasing union of wellfounded Borel partial orders if and only if it admits an (injective) Borel homomorphism to the eventual domination order.

math.LO↗