🏅 Top traders

https://mathstodon.xyz/@tao/111526765350663641

"The #Lean4 project to formalize the proof of the Polynomial Freiman-Ruzsa conjecture has succeeded after three weeks, with the dependency graph completely covered in a lovely shade of green: https://teorth.github.io/pfr/blueprint/dep_graph_document.html , and the Lean compiler reporting that the conjecture follows from standard axioms."

@kiudee Yep, Tao posted on Zulip saying it was complete as well, and as no one seems to disagree, that makes this resolve now. Thanks everyone!

Now only `total-dist` to go, which is https://github.com/teorth/pfr/blob/d97782fc789a5c9d41854f8247159bb1a3c87732/PFR/Endgame.lean#L449

`lem-bsg` is claimed by Yaël and Bhavik per https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Outstanding.20tasks.2C.20version.204.2E0 ; term finishes on 1st Dec (https://www.cam.ac.uk/about-the-university/term-dates-and-calendars) and my bet is that Yaël won't be able to resist cracking on with it as soon as term ends ;) Paul Lezeau is an unknown quantity to me, but the PR for the distance increment bound is https://github.com/teorth/pfr/pull/108 .

So shouldn't the later dates be higher than the more recent dates?

@asmith Yeah oops - later dates are guaranteed to resolve YES if earlier ones do, thanks for catching that. Feel free to correct it yourself.

Note to self and others: When Kevin publishes a blueprint for his FLT project, we should make a big multi-market on all the subgoals he puts in.