Researchers used AI models to reduce a formal proof in Lean code by 24.65%, shrinking it from 151,287 to 113,990 lines while preserving the theorem statement and passing kernel verification. The experiment demonstrates how AI agents can optimize existing proofs through iterative refinement and code reuse over several hours of work.