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

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.

The crisis of AI-generated mathematics
Max Weinreich
arXiv18 Oct 2026PreprintarXiv licenceFull textGeneral mathematicsarXiv
What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics
Ying Xie
arXiv12 Oct 2026PreprintCC BY 4.0Full textGeneral mathematicsarXiv
Proof Perplexity: A Probabilistic Approach to Measuring non-triviality in Machine Generated Proofs
Madhuparna Das, Soumya Banerjee
arXiv15 Oct 2026PreprintCC BY 4.0Full textLogic & foundationsarXiv
The occupation time of a random walk generated by the uniform random permutation--a GPT-6 Astra proof
Wenpin Tang
arXiv20 Sep 2026PreprintarXiv licenceFull textProbabilityarXiv
Statistical Theory in the Age of Machine-Assisted Mathematics: Rethinking How Theory Is Made and Taught
Pietro Coretto
arXiv3 Sep 2026PreprintarXiv licenceFull textStatisticsarXiv

Cite

BibTeX RIS

BibTeX

@misc{aryal2026studying,
  title = {{Studying proof data with proof theory: the case of AI-generated mathematics}},
  author = {Safal Raman Aryal},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.25357},
  eprint = {2610.25357},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.25357},
  note = {CC BY 4.0},
}

RIS

TY  - UNPB
TI  - Studying proof data with proof theory: the case of AI-generated mathematics
AU  - Safal Raman Aryal
PY  - 2026
DA  - 2026/10/18
PB  - arXiv
DO  - 10.48550/arxiv.2610.25357
UR  - https://arxiv.org/abs/2610.25357
AB  - 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.
ER  -

Abstract

Related

Cite