Zulip Chat Archive

Stream: new members

Topic: Quadratic, cubic, and quartic formulas


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 06 2020 at 17:39):

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

view this post on Zulip Benjamin (Sep 06 2020 at 17:40):

Is that a no to all three?

view this post on Zulip Johan Commelin (Sep 06 2020 at 17:40):

Probably quadratic is around somewhere...

view this post on Zulip Kenny Lau (Sep 06 2020 at 18:23):

docs#quadratic_eq_zero_iff

view this post on Zulip Kenny Lau (Sep 06 2020 at 18:24):

I got this by searching for quadratic

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Alex J. Best (Sep 07 2020 at 01:06):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 01:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 07 2020 at 01:34):

y is the square root of some subexpression

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Benjamin (Sep 07 2020 at 01:36):

I see thanks

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 02:00):

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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 02:02):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 06:08):

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

view this post on Zulip 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