Comment by jboggan

Well I'm sure some people (maybe me if I had time) will do a write-up of this proof. It treads familiar ground for most of the setup, it's mostly the disk lemma and cancellation calculations that need to be understood, it's a fairly short paper and quite tractable.

I think it helps that basically everyone thinks this conjecture is true, it's just been so darn weird to attack. There's this odd thing that the induction proofs of this problem kept running into, which is that the N+1 condition would work except for in one tiny case when it could fail, but it would be covered by a very slightly stronger version of the conjecture. But then that would fail on one tiny case in induction, but you could solve that with another slightly stronger version. Etc., etc. I almost wondered if there were some sort of structure to the increasingly strong conditions and wanted to prove something about the meta-induction between the stronger conditions and the N's that they needed the next level to remain true. But that failed after 5 steps I think (Fable actually helped me write a few hundred test cases to explicitly show that pattern didn't continue forever, thank God).

BTW my existing test suite from previous proof attempts jives with this new algorithm, so I haven't seen any evidence yet that it's incorrect. Waiting for a Lean proof obviously.