AI-generated formal proofs use less logical compression than humans
Studying proof data with proof theory: the case of AI-generated mathematics
Logic in Computer Science
Summary
The paper studies how mathematics proofs created by AI differ from those made by humans. The authors find that AI-generated proofs tend to be longer and less efficient compared to human-written ones. This shows that AI does not yet match the way humans compress and simplify logical steps in proofs. The study uses measurements from automated proof tools to compare AI and human proofs.
What this means in practice
- •For automated prover developers: Identify areas where AI-generated proofs are inefficient to improve automated proof optimization tools.
- •For formal verification engineers: Assess AI-generated proofs in formal verification processes to ensure proof quality and efficiency.
Authors
Safal Raman Aryal
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.