## Stream: new members

### Topic: Quadratic, cubic, and quartic formulas

#### Benjamin (Sep 06 2020 at 17:39):

Does mathlib have theorems for the quadratic, cubic, or quartic formulas? If not, I'm curious if it'd be feasible for a Lean beginner to prove them.

#### Johan Commelin (Sep 06 2020 at 17:39):

Nope, we don't. Sounds like a nice first project

#### Benjamin (Sep 06 2020 at 17:40):

Is that a no to all three?

#### Kenny Lau (Sep 06 2020 at 18:24):

I got this by searching for quadratic

#### Alex J. Best (Sep 06 2020 at 19:15):

Sounds good! Might be best to work in complex or an algebraically closed field for the cubic and quartic versions though.
Actually the quadratic one could have a version for any characteristic not 2 field (not just a linear ordered field).

#### Kevin Buzzard (Sep 06 2020 at 22:01):

Yes, I got one of my kids to implement the quadratic formula as part of their work experience and they did it for any field of characteristic not 2, and the statement was that if the discriminant has a square root then...

#### Benjamin (Sep 07 2020 at 00:03):

Would it be preferable to implement the solutions in terms of the discriminant like was done for the quadratic case, or to just list the solutions directly in terms of the coefficients?

#### Alex J. Best (Sep 07 2020 at 01:06):

I would say assume algebraically closed and express it in terms of the coefficients.

#### Mario Carneiro (Sep 07 2020 at 01:19):

The way I expressed the core version of the quadratic/cubic/quartic formulas in metamath is to have a hypothesis saying things like x^3 = ... and y^2 = ..., so that the main proof can be done in any ring with characteristic not 2 or 3.

#### Alex J. Best (Sep 07 2020 at 01:22):

I guess having both as part of the API isn't actually much harder anyway, http://us.metamath.org/mpegif/cubic.html

#### Mario Carneiro (Sep 07 2020 at 01:23):

I don't think we have a nice way to work with nth roots over algebraically closed fields right now, but you could specialize this theorem to real using real.sqrt and real.rpow

#### Mario Carneiro (Sep 07 2020 at 01:23):

the core version I mentioned is http://us.metamath.org/mpegif/cubic2.html

#### Mario Carneiro (Sep 07 2020 at 01:25):

it's more general anyway, since it allows you to pick either the positive or negative square root, or any of the three cube roots in an alg closed field

#### Mario Carneiro (Sep 07 2020 at 01:26):

You might be amused by http://us.metamath.org/mpegif/quartfull.html, where all substitutions are performed into the quartic formula

#### Benjamin (Sep 07 2020 at 01:34):

Mario Carneiro said:

The way I expressed the core version of the quadratic/cubic/quartic formulas in metamath is to have a hypothesis saying things like x^3 = ... and y^2 = ..., so that the main proof can be done in any ring with characteristic not 2 or 3.

What is y here?

#### Mario Carneiro (Sep 07 2020 at 01:34):

y is the square root of some subexpression

#### Mario Carneiro (Sep 07 2020 at 01:35):

for example, for the quadratic formula instead of writing +- sqrt (b^2 + 4*a*c) you have a hypothesis y^2 = b^2 + 4*a*c and then use y

#### Mario Carneiro (Sep 07 2020 at 01:35):

you will end up with a disjunction like x = (-b + y) / 2*a \/ x = (-b - y) / 2*a

I see thanks

#### Mario Carneiro (Sep 07 2020 at 01:38):

that way you don't need to know that square roots actually exist in the ring you are working over, since you are given whichever roots you need, but to use the theorem you have to provide a root or else it is trivial. I'm not sure exactly under what conditions you can reverse the implication and prove that the root exists given a root of the quadratic

#### Benjamin (Sep 07 2020 at 01:44):

I'm not very good at reading metamath proofs (or formal proofs in general yet), but did you basically proceed by plugging in the equations to the polynomial to verify that they're roots? And then how did you prove that they are the only solutions?

#### Mario Carneiro (Sep 07 2020 at 01:48):

No, the proof does not jut plug in the solutions, because it's easier to just maintain the biconditional at all times. The proof strategy is to perform things like "subtract on both sides" or "multiply by a nonzero constant" which preserve the biconditional, algebraic expansions (which preserve equality, and could be done by ring), and the key fact x^2 = y^2 <-> x = y \/ x = -y and a similar version for cube roots.

#### Mario Carneiro (Sep 07 2020 at 01:49):

You could plug in the solutions but that's a lot of expansion work and it won't make the reverse direction any easier

#### Mario Carneiro (Sep 07 2020 at 01:50):

I of course didn't invent the proof; Cardano has the claim I believe. Wikipedia has an overview of it

#### Mario Carneiro (Sep 07 2020 at 02:00):

The metamath proof cubic proves $ax^3+bx^2+cx+d=0$ by reducing it to mcubic, which proves $x^3+ax^2+bx+c=0$ by reducing it to dcubic, which proves $x^3+px+q=0\iff \exists r(r^3=1\land x=rt-m/rt)$ (where $m$ and $t$ are formulas in terms of $p,q$), by plugging into the equation in the reverse direction (dcubic1), and for the forward direction (dcubic2) first solving the equation $x=u-m/u$ for $u$, and then using it to derive an equation for $r$.

#### Mario Carneiro (Sep 07 2020 at 02:02):

I think this is a version of Vieta's substitution on wiki

#### Benjamin (Sep 07 2020 at 03:31):

Thanks, this is helpful. I probably won't get to this for a while (if at all). I'm still learning Lean, but if I get around to trying to contribute to mathlib this is what I'll try.

#### Kevin Buzzard (Sep 07 2020 at 06:08):

It's a great thing to work on for a beginner

#### Kenny Lau (Sep 07 2020 at 06:41):

Ian Stewart's book on Galois Theory has a proof using Galois Theory

Last updated: May 16 2021 at 05:21 UTC