Integration with mathlib

Stream: FLT

[Kevin Buzzard]

I am unclear about how much stuff from the FLT project should be in mathlib. For example, the Frey curve is an elliptic curve which doesn't exist. You build it from a counterexample to FLT (easy) and then you prove that it has too many nice properties to actually exist (2000 pages of hard work). Do we want the Frey curve in mathlib? I'm very very happy to start PRing. No doubt there will be some "work in progress" stuff in the FLT repo which is nowhere near mathlib-ready, but the Frey curve stuff will certainly be ready and stable quite soon; the point is that it's not really a thing which is useful for anything but FLT, and it's certainly not studied independently. The main but straightforward theorem is that the p-torsion in the Frey curve coming from a counterexample a^p+b^p=c^p from FLT has lots of very nice properties, and the hard theorem is that nothing has these properties.

[Kim Morrison]

I would suggest the Frey curve stays in FLT!

[Michael Stoll]

Frey curves are used to solve other diophantine equations, too (e.g., of generalised Fermat type), so it would be reasonable to have some results about them in Mathlib eventually.

[Kevin Buzzard]

@Michael Stoll you might then have some opinions about my formalisation of it, because I demanded some congruences on A,B,C mod powers of 2 and then specifically used the global minimal model rather than Y^2=X(X-A)(X+B).

[Michael Stoll]

I think it is fine to first do it with the specific form needed for FLT and later think about how to generalise it so that it will be useful in other situations. My point is that we should keep this in mind (and so maybe try to keep the statements as general as possible if this can be done without sacrificing simplicity).

[Mario Carneiro]

Silly question: isn't the whole point that Frey curves are impossible objects? In that case, what applications would they have except in their nonexistence?

[Mario Carneiro]

To me this suggests that Frey curves are a concept limited in usefulness to the proof of FLT, and we should try to make as many theorems not specific to them as possible (except for the ones along the "spine" of the contradiction proof), so that they can be used even outside the contradictory context used for most of FLT

[Rida Hamadani]

Maybe the Counterexamples folder of mathlib is a good place for Frey curves to live?

[Mario Carneiro]

only if we're willing to upstream all of FLT to Counterexamples...

[Damiano Testa]

First division by zero, now counterexamples to FLT: sometimes formalisation seems like it wants people to laugh at it...

[Joseph Myers]

I take a maximalist view of the scope of mathlib: FLT is known mathematics that might occasionally get applied in other proofs, so it belongs in mathlib proper (not Archive or Counterexamples), and thus all its dependencies belong in mathlib proper as well; the main question is how to tell when such dependencies are ready to go in mathlib.

[Riccardo Brasca]

In my opinion it is rather important to not let the for_mathlib folder becoming gigantic, by PRing stuff to mathlib. This of course slow down the project a little, but in the long run it pays off. Otherwise bumping mathlib can be a very tedious and time consuming job.

[Kevin Buzzard]

My plan was not to let it ever have size more than epsilon. Right now we have some work on Hopf algebras which Amelia is PRing to mathlib. Please feel free to review #11962 and #11970 !

[Kevin Buzzard]

I think that with things like LTE it was tempting to grow for_mathlib when the end became in sight; however the end will not be in sight for many years here.

[Kim Morrison]

It might be good to work out how to maintain a visible / rewarding-to-look-at PR queue for FLT relevant stuff.

[Kim Morrison]

Maybe just an FLT label for Mathlib PRs?

[Kim Morrison]

That way reviewers who are excited about FLT can review those first.

[Kim Morrison]

• a topic in this stream where FLT-relevant mathlib PRs can be mentioned