Lean4 collaboration

Stream: general

[don]

Hi folks! I'm creating a website for lean where one can submit large unsolved Lean4 problems and have other users submit proofs for it (possibly partial or full). Curious if there's good candidate problems that have this particular structure, or if any prior attempts have been done before?

[Kevin Buzzard]

Here's one: https://github.com/ImperialCollegeLondon/FLT/blob/7e7bb422fd0186c6abca6cdfa058aa3504ebcf20/FLT/AutomorphicForm/QuaternionAlgebra/FiniteDimensional.lean#L20

The informal proof is documented here .

Here's a harder one: https://github.com/ImperialCollegeLondon/FLT/blob/7e7bb422fd0186c6abca6cdfa058aa3504ebcf20/FLT/Basic/Reductions.lean#L324 . The proof of this is a 100+ page paper by Mazur. A sketch is available in this lecture.

In the #FLT channel we are doing exactly what you propose, just without the website.

[Kim Morrison]

@don, perhaps it would be helpful to explain what differentiates your plan from "a git repository with Lean code containing sorry" (i.e. what Kevin is implicitly saying is the existing solution to this problem).