Proving Pell's equation is solvable

Stream: Is there code for X?

[Gareth Ma]

Hi, as thread name suggests, is there code for proving pell's equation has non-trivial fundamental solutions? I only found related code in number_theory/pell.lean, but inside it only proves the special case d = a^2 - 1 for x^2 - dy^2 = +-1. If not, I would like to make progress on this! However, it seems like a large project to me, so if anyone can give me some directions on where to start then that will be great. Do I just follow some textbook / notes and grind through the lemmas one by one? Thanks! :)

[Gareth Ma]

And also I guess, how do you guys approach adding large contributions? I was working on a proof on some other theorem the past few days (which turned out to be in mathlib already...), and handling 300 lines of code in a single file is already making me dizzy haha.

[Kevin Buzzard]

I believe that @Michael Stoll has a student working on this. I also had a student which proved the existence of solutions but they didn't push it to mathlib, it was just a student project.

[Gareth Ma]

Alright, I will see if there are any interesting places to work on. I am also only an undergraduate student haha :)

[Kevin Buzzard]

It's quite hard to find low-hanging fruit in elementary number theory nowadays. One thing we don't have is Dirichlet's units theorem, a far-reaching generalisation of Pell. A PhD student of mine needs it for their proof of the Mordell-Weil theorem.

[Kevin Buzzard]

I would look at the situation differently. It's now rather difficult to contribute to mathlib as an undergraduate; perhaps the best idea might be to choose something from the undergrad todo list, although please open a discussion before embarking on something because there will be opinions about how to set up definitions, or half-finished work you can build on etc. The other situation is that adding anything to mathlib right now is kind of tricky because we are in the middle of porting the entire library to lean 4. I would encourage you to work on standalone projects (like your Mersenne project, which is a great way to get into Lean) and just formalise what the heck you want, e.g. just do Pell -- who cares if someone else did Pell. Do it, add it to the Mersenne stuff, write a little write-up about it and stick it online. This will buy the community some time to get the port done ;-)

[Gareth Ma]

Hahahaha that definitely sounds great too, maybe I can work on some projects then write a blog or two on it, since I am definitely learning a lot and it is a very interesting topic :) Thanks for your suggestions!

[Michael Stoll]

Just to confirm what @Kevin Buzzard mentioned earlier: I do have a student working on Pell's equation. He does in fact have a sorry-free proof of the existence of non-trivial solutions, which he is in the process of cleaning up somewhat. My plan is to then clean it up further to make it mathlib-ready and add it to mathlib at some point.

[Oliver Nash]

If somebody wants to fill gaps in elementary number theory then I think it would be great to add some of the classical results about asymptotic growth of arithmetic functions. For example, that $d(n) = n^{o(1)}$ see here and here or $n^\epsilon/\varphi(n) = o(1)$ for $\epsilon < 1$.

[Kevin Buzzard]

@Bhavik Mehta how much of that stuff got done in unit fractions?

[Oliver Nash]

I just added a link to the message above with a weak bound but they have full formalisations of stronger bounds directly above!

[Eric Rodriguez]

Kevin Buzzard said:

It's quite hard to find low-hanging fruit in elementary number theory nowadays. One thing we don't have is Dirichlet's units theorem, a far-reaching generalisation of Pell. A PhD student of mine needs it for their proof of the Mordell-Weil theorem.

I had some idea in my head that someone was actually working on this already

[Anne Baanen]

We had been considering continuing our diophantine project towards the units theorem, but I don't think we have any concrete progress towards that.

[Xavier Roblot]

I have been working the proof of Dirichlet's theorem lately (although I also spent too much time having fun porting files to mathlib4 :smile:).
I am almost finished proving the results for lattice theory that are needed and so I should able to start working on the final stage soon.

[Gareth Ma]

I am interested in that, though I am not sure what should be added to mathlib and what shouldn't. For example, things like Mertens' estimate and various sieve estimates (which depends on other useful elementary estimates) are proven in the Unit Fractions project, in particular lemma 2.7 and 2.8. However, those weren't added to mathlib

[Gareth Ma]

Though I can always work in a separate project first then ask when I get some progress :P

[Eric Rodriguez]

cc @Bhavik Mehta

[Bhavik Mehta]

Lots of the stuff in the basic estimates file ought to be in mathlib, the reason it's not is a combination of me not having time, and some unclear questions about where it should go and how it should be structured, eg what's the correct mathlib version of partial summation which is usable as a tool for analytic number theory

[Michael Stoll]

I have now a 70-line proof ready of the following:

theorem pell.ex_nontriv_sol {d : ℤ} (h₀ : 0 < d) (hd : ¬ is_square d) :
  ∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Is there support for adding this result to mathlib now?

[Mario Carneiro]

it depends on where it lies with respect to the frontier of ported files

[Michael Stoll]

If so, the question is where this is supposed to go. Everything that is done in number_theory.pell has the assumption d = a^2 - 1 pretty much baked in -- it starts with the lines

parameters {a : ℕ} (a1 : 1 < a)

include a1
private def d := a*a - 1

and epxresses everything in terms of a instead of d (which is d a1 in the file).
So it would be difficult to adapt it to the general case (at least without a major refactor).
My suggestion would be to

• move number_theory.pell to number_theory.pell.special (in particular, set up a subfolder pell)
• add a new file number_theory.pell.general that contains the new result and can be expanded (and may perhaps eventually also include the material that is now in number_theory.pell as special cases)

[Mario Carneiro]

If it depends on stuff that has already been ported you would probably be better off PR'ing it directly to mathlib4

[Mario Carneiro]

You might also consider making the number_theory.pell theorem depend on yours

[Eric Wieser]

Mario Carneiro said:

If it depends on stuff that has already been ported you would probably be better off PR'ing it directly to mathlib4

This requires either porting manually or working out how to setup mathport one-shot, right? Vs PRing to mathlib3 where the actual porting is automatic.

[Michael Stoll]

According to this (was there a linkifier shortcut?), there are still 27 or so dependencies missing.

[Mario Carneiro]

for a 70 line just-written proof I imagine porting manually isn't too hard

[Eric Wieser]

was there a linkifier shortcut?

port-status#path/to/file

[Mario Carneiro]

apparently number_theory.pell is one of the dependencies too

[Michael Stoll]

Right now, it is just a stand-alone statement and proof, which imports tactic.qify, data.zmod.basic and number_theory.diophantine_approximation.

[Michael Stoll]

Mario Carneiro said:

apparently number_theory.pell is one of the dependencies too

OK, then make it 26 :smile:

[Michael Stoll]

Of course, the theory around it should also be built (group structure &c)...

[Michael Stoll]

The chain of unported files to port-status#number_theory/pell has length ~17.

[Mario Carneiro]

how does this happen :sob: I know that file has abnormally low dependencies for mathlib

[Mario Carneiro]

what does the port-status PDF picture for it look like?

[Michael Stoll]

I guess this is spoiled by number_theory.zsqrtd.basic ..

[Mario Carneiro]

that was just int, twice

[Michael Stoll]

Click on "show graph" on the page linked above.

[Mario Carneiro]

it used to be 100 lines at the top of pell

[Mario Carneiro]

unfortunately the graph on the web page doesn't include the gray nodes from the original version

[Michael Stoll]

Yeah, I would assume that much of the imports is not actually needed (like tensor products...).

[Mario Carneiro]

that is to say, I would expect that of those 26 unported dependencies, 25 of them are gray nodes for pell

[Michael Stoll]

In any case, my proof depends on port-status#number_theory/diophantine_approximation, which is still quite a bit away from the frontier.

[Eric Wieser]

Mario Carneiro said:

unfortunately the graph on the web page doesn't include the gray nodes from the original version

Yes, these are far too expensive to calculate for all 3000 files every 30 minutes

[Eric Wieser]

Or at least, we'd need a better approach to do it than iterating the current approach 3000 times!

[Michael Stoll]

Let me note in passing that using this, together with #18460 (which could do with some reviewing), it would be easy to show that every positive solution to Pell's equation for $d$ comes from a convergent of the continued fraction expansion of $\sqrt{d}$...

[Eric Wieser]

Mario Carneiro said:

how does this happen :sob: I know that file has abnormally low dependencies for mathlib

#18468 attempts to cut this path a bit

[Eric Wieser]

This PR is now passing CI

[Michael Stoll]

I have now made a PR with the existence theorem (#18484). It just adds a new file number_theory.pell_general containing the result. The 75 lines containing the docstring, statement, and proof correspond to 25 lines in Ireland-Rosen, so the de Bruijn factor is not too bad...

[Michael Stoll]

With some more golfing by @Thomas Browning, it is now down to 66 lines.
I have also added a link to 100.yaml.

[Michael Stoll]

@Oliver Nash suggested to rename number_theory.pell to ...pell_matiyasevic and ...pell_general to ...pell. This is done in #18503, together with some updating of the documentation.

[Michael Stoll]

By now, I have written code to show that the solution set consists of the powers (with integer exponents) of a fundamental solution (up to sign) w.r.t. to the usual group structure on the solution set. The next PR, #18567, is just a small addition to show that a positive solution exists, which will be used to define the fundamental solution.

[Alex J. Best]

Mario Carneiro said:

how does this happen :sob: I know that file has abnormally low dependencies for mathlib

one way this happens is that there are a bunch of lemmas in the original pell file that were ad-hoc specializations / repetitions of lemmas that later appeared in the library in a more natural location, if later people come and replace these with replace these with references to the library versions so the library doesn't contain multiple versions of the same thing, then the dependencies go up

[Mario Carneiro]

indeed, the extent to which that is a tradeoff is not really appreciated in the normal review process

[Mario Carneiro]

because make no mistake, that is actively making mathlib worse for certain applications (users that don't want to import hundreds of files for a basic result and came to mathlib because it is the canonical source for these kinds of theorems)

[Alex J. Best]

well those users could simply pin an older version if the material is stable and not being actively developed?

[Johan Commelin]

Mario, are you contradicting your t-shirt?

[Kevin Buzzard]

Why would a user not want to import hundreds of files for a basic result? Every lecture I've given this term has started import tactic and many of them then import one or two other files so that the material works. Under the hood it would not surprise me if I'm importing hundreds if not thousands of files every lecture but I've never seen a down side to this.

[Alex J. Best]

Generally the cohesiveness and non-silod nature of mathlib is touted as a good thing!

[Kevin Buzzard]

On day one of an analysis lecture the lecturer imports the real numbers and makes no apology, and also doesn't make any attempt to explain what's going on under the hood -- they just say "here's the API".

[Mario Carneiro]

Alex J. Best said:

Generally the cohesiveness and non-silod nature of mathlib is touted as a good thing!

I don't think this has to come at the cost of cohesiveness at all. You can have a basic definition of Real and then prove it is equivalent to the fancy definition in a fancy file

[Mario Carneiro]

In a lot of computational applications you need to make a specialized representation of e.g. polynomials and then prove they are representable by the abstract version afterward; in this situation usually the computational model will have few dependencies and the proofs will depend on the more complex abstract polynomial file

[Kevin Buzzard]

If I am interested in computational applications of Pell then lean would not be my first choice of system :-)

[Mario Carneiro]

Kevin Buzzard said:

On day one of an analysis lecture the lecturer imports the real numbers and makes no apology, and also doesn't make any attempt to explain what's going on under the hood -- they just say "here's the API".

Kevin, this approach is very specific to classroom teaching. I don't think it works for substantial developments on top of std/mathlib, especially other libraries

[Kevin Buzzard]

I don't really understand why another library cares whether it's importing ten files or 1000

[Kevin Buzzard]

Disclaimer: I am not a computer scientist

[Kevin Buzzard]

I want all the theorems :-)

[Mario Carneiro]

I do too, but not if it takes 6 hours and a larger machine than I have to compile

[Johan Commelin]

Mario, the current "use a mathematical hammer" approach is trying to keep the compile time of all of mathlib as low as possible.

[Mario Carneiro]

and yet, it keeps growing

[Johan Commelin]

If we keep around all the low-tech versions, then they only add more to that growing number.

[Mario Carneiro]

and is already much larger than the stomachs of most computer scientists

[Mario Carneiro]

the thing is, most people don't care about most of mathlib

[Mario Carneiro]

and the current structure means most people have to depend on most of mathlib

[Johan Commelin]

Those computer scientists should grab a copy of EGA from their local library, brew a pot of tea, and try to "compile" it (-;

[Kevin Buzzard]

The nature of mathematics is that beyond some point it becomes a hugely interconnected mess. The statement of FLT can be made in core but the proof is going to require importing the vast majority of what we have now

[Kevin Buzzard]

And a heck of a lot more

[Mario Carneiro]

that's fine, if things are actually used then they should be dependencies

[Kevin Buzzard]

I think we can avoid ZFC and the game theory stuff but most of the rest is on the radar :-)

[Mario Carneiro]

the thing is we have huge quantities of unnecessary stuff getting pulled in most of the time

[Kevin Buzzard]

Yes! Isn't it great that computers are so good now!

[Johan Commelin]

"actually used" is almost always up for debate.

[Kevin Buzzard]

My operating system pulls in huge quantities of unnecessary stuff but I'm not complaining

[Mario Carneiro]

I complain a lot about that too

[Kevin Buzzard]

I can read my email and that's fine

[Johan Commelin]

Kevin Buzzard said:

I can read my email and that's fine

I complain a lot about that too

[Kevin Buzzard]

Actually I'm not very good at reading my email but I can't blame my operating system for this.

[Kevin Buzzard]

But let's get back to Pell! How do we get a minimal setup for computing it but then import more stuff for proving it? What does that setup look like?

[Mario Carneiro]

Johan Commelin said:

"actually used" is almost always up for debate.

"transitively reachable from the proof term" is clearly an upper bound on it though, and we have hard data on how prevalent that is

[Mario Carneiro]

Re: pell, I think the only obvious example of such a thing was the Z[√d] construction

[Johan Commelin]

So you are not complaining about low-tech proofs getting replaced by high-tech proofs. But just about the fact that our coarse import strategies pull in so much junk that isn't used?

[Mario Carneiro]

Yes to the second, it depends to the first

[Mario Carneiro]

low-tech -> high-tech is a tradeoff, is it worth reducing the size of mathlib by X in exchange for increasing the dependency cost of this file and all its dependents by Y

[Mario Carneiro]

As long as a decision is made with eyes wide open to the costs, I'm okay with either approach

[Mario Carneiro]

Note that std contains a number of theorems about ordering on Nat that are literally copy-pasted from theorems about LinearOrder

[Mario Carneiro]

this is a deliberate duplication of work in order to make it possible to work with Nat without a huge stack

[Kevin Buzzard]

I always found it fascinating in mathlib3 that data.nat.basic imported a vast amount of stuff -- somehow that was not what I would have guessed.

[Kevin Buzzard]

But I wasn't losing any sleep over it :-)

[Mario Carneiro]

that makes one of us

[Oliver Nash]

Surely it's possible to create a tool which consumes a definition / lemma in Mathlib and emits a new source tree which includes exactly those definitions and lemmas which it needs?

This wouldn't solve the problem of dependencies that exist because some very general definition / lemma is being applied in a trivial situation but it could still be useful / interesting (and one could imagine an even more powerful tool which also attacks this).

One of the benefits of having a library of mathematics that is understood by a computer should be that we can manipulate the mathematics in useful ways.

[Mario Carneiro]

Sure, I've even written a tool like that before (not for lean though). It's somewhat harder to do on lean source because of tactics and annotations

[Mario Carneiro]

Most kinds of semantic processing on lean source require compiling it though, which means that you might have to pay the costs anyway

[Mario Carneiro]

At a file level it is definitely possible with minimal analysis, and I would like mathlib4 to be usable in this way. Early on I was pushing for lake to be able to create ad-hoc packages by tree-shaking files from mathlib4 so that std doesn't need to exist

[Mario Carneiro]

at this point it looks unlikely to happen in the near term but it is not a fundamentally hard problem

[Mario Carneiro]

but for that kind of thing to be useful mathlib would need to change its ways to have a less tangled structure, smaller files and more stratification

[Kevin Buzzard]

smaller files is something we can probably all agree on.

[Michael Stoll]

Not to distract from this important discussion too much :smile: -- here is the next PR: #18568.
It defines a type for the solutions and provides it with a group structure and compatible negation.

[Eric Wieser]

For those following this thread but not the PR; I've argued in that PR that we might not need a new type, and could just use unitary (sqrt d) instead. To be able to do that, we need the hopefully non-controversial #18572.

[Eric Wieser]

It probably also makes sense to generalize docs#pell.is_pell to an arbitrary d (and move it from number_theory.pell_matiyasevic to number_theory.pell)

[Michael Stoll]

Thanks @Eric Wieser for the refactor zsqrtd.conj --> star.
Some comments regarding the general approach:

• I think it makes sense to have a separate type for solutions to the Pell equation (which can be unitary (zsqrtd d) under the hood) and provide an API for it. E.g., I want to think of a solution as a pair (x, y) of integers and not necessarily as the element x + y √d of zsqrtd d -- writing a.re and a.im is not very intuitive in this context, for example.
• I would like to develop the general theory "in the right way" (what this is may certainly be debatable) first, before refactoring what is now in number_theory.pell_matiyasevic.

[Eric Wieser]

Regarding your second point; I think it would make sense to first move all the stuff in pell_matiyasevic that isn't actually restricted to d = a*a - 1 to the pell file; and only then develop things the right way

[Eric Wieser]

It might be that that's only the definition of is_pell and little else

[Michael Stoll]

Even is_pell is written in terms of a:

 def pell.is_pell {a : ℕ} (a1 : 1 < a) : ℤ√↑(d a1) → Prop := ...

(this is how the HTML docs show it; it is not as apparent in the source...)

[Michael Stoll]

My point is that it would be rather painful to try to do this in parallel, since d = a^2 - 1 is really pretty much hard-coded in pell_matiyasevic.

[Michael Stoll]

The first few relevant lines in pell_matiyasvicare

parameters {a : ℕ} (a1 : 1 < a)

include a1
private def d := a*a - 1

So there is literally nothing in this file that is not tied to this special case.

[Eric Wieser]

I'm not explaining what I mean very well, so I made #18573. It looks like barely anything generalizes though, so I think it's fine to ignore is_pell for your current work (although I think #18573 is good to have anyway).

[Michael Stoll]

#18626 is the next PR in this sequence. It adds some API lemmas for Pell solutions, which I need to be able to define what a fundamental solution is and to prove some properties later.

[Michael Stoll]

#18901 defines fundamental solutions and proves their existence and uniqueness and that the fundamental solution (essentially, i.e., up to a sign) generates the group of solutions (and is characterized by this property).
Reviews welcome!

[Michael Stoll]

Any further comments on #18901 ?

[Michael Stoll]

#19010 is a small PR that just fixes two lemma names in the module docstring (so that doc-gen links them correctly).