## Stream: new members

### Topic: Bezout's identity

#### Brian Jiang (Mar 22 2020 at 17:08):

I've been trying to prove Bézout's identity, but am stuck on the fact that the normal proof involves using the Euclidean algorithm indefinitely

#### Brian Jiang (Mar 22 2020 at 17:08):

Can someone give a few hints on how to start/proceed?

#### Kevin Buzzard (Mar 22 2020 at 17:09):

I'm not sure that proofs are allowed to be indefinitely long, in mathlib or otherwise :-)

#### Kevin Buzzard (Mar 22 2020 at 17:09):

Did you look at the proof which is already in mathlib?

#### Brian Jiang (Mar 22 2020 at 17:11):

whoops I meant that it uses the Euclidean algorithm until there is no remainder left

#### Brian Jiang (Mar 22 2020 at 17:11):

I'll take a look, thanks!

#### Kevin Buzzard (Mar 22 2020 at 17:11):

right, so it basically uses induction.

#### Kevin Buzzard (Mar 22 2020 at 17:13):

I haven't looked at what is in the repo, but if b<=a then you could prove that gcd(a,b) is a Z-linear combination of a and b by strong induction on a, and the inductive step could be done by observing that gcd(a,b)=gcd(a-b,b)

#### Mario Carneiro (Mar 22 2020 at 17:16):

The way it is done in mathlib is to slightly modify the definition of gcd to calculate the coefficients at the same time as it is doing the euclidean division

#### Brian Jiang (Mar 22 2020 at 17:17):

by mathlib do you mean the github page?

#### Brian Jiang (Mar 22 2020 at 17:17):

sorry Im having a little trouble finding it

#### Mario Carneiro (Mar 22 2020 at 17:17):

https://github.com/leanprover/mathlib/

#### Kevin Buzzard (Mar 22 2020 at 17:17):

Do you have a Lean project set up and a working leanproject command?

#### Mario Carneiro (Mar 22 2020 at 17:18):

That is, the work needed to prove gcd exists in the first place is about the same as that needed to prove that it is a linear combination of the inputs

#### Kevin Buzzard (Mar 22 2020 at 17:20):

Here is the theorem in mathlib but if you have set up a Lean project with mathlib as a dependency then all that code is on your computer already.

alright, thanks

#### Kevin Buzzard (Mar 22 2020 at 17:20):

They prove a constructive version of Bezout there, i.e. they actually come up with functions $\lambda(a,b)$ and $\mu(a,b)$ such that $d=\lambda(a,b)a+\mu(a,b)b$.

#### Kevin Buzzard (Mar 22 2020 at 17:22):

this is what gcd_a and gcd_b are. They can't call them $\lambda$ and $\mu$ because $\lambda$ is already used up for $\lambda$-calculus :-)

#### Mario Carneiro (Mar 22 2020 at 17:25):

actually I think the idea behind the naming convention is that gcd_a x y and gcd_b x y are $a$ and $b$ in the equation $gcd(x,y)=ax+by$

#### Mario Carneiro (Mar 22 2020 at 17:28):

Hm, my name should be on that file, it looks like the proof got transplanted from another file and the attribution got separated from it

#### Patrick Massot (Mar 22 2020 at 17:31):

In France, Bézout's theorem is $ua + vb = \mathrm{pgcd}(a, b)$ so I always found mathlib utterly confusing hehre.

#### Mario Carneiro (Mar 22 2020 at 17:32):

we could change the names to gcd_u and gcd_v. There seems to be no name that is at all descriptive

#### Mario Carneiro (Mar 22 2020 at 17:32):

Clearly the letter pairs are not allocated reliably

#### Patrick Massot (Mar 22 2020 at 18:35):

I don't have a good solution here (and I don't think we should spend too much time thinking about this).

#### Bryan Gin-ge Chen (Mar 23 2020 at 00:06):

Mario Carneiro said:

Hm, my name should be on that file, it looks like the proof got transplanted from another file and the attribution got separated from it

https://github.com/leanprover-community/mathlib/pull/2217

#### Mario Carneiro (Mar 23 2020 at 02:53):

thanks!

Last updated: May 11 2021 at 13:22 UTC