Comment by pyentropy

Not a Lean expert but some of the proof tactics used to prove are probably novel? Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?