Descartes Rule of Signs

Stream: Is there code for X?

[Taylor Belcher]

Hi all,
I am leading a few first year students (they are advanced high schoolers, equivalent to about first year undergrads halfway done with freshman year) in a project this summer and I am looking for a topic they can wrestle with. The list of 100 theorems on the Lean community website (https://leanprover-community.github.io/100-missing.html) lists Descartes' Rule of Signs as still missing. This seems like a possible direction to take my students. Does anyone know if anyone is already working on this?
Thanks.

[Johan Commelin]

I don't know of anyone actively working on this. I think it's a nice project. Note that there are also some interesting variants of the rule of signs.

[Adam Topaz]

I think this sounds like a great project! (As for generalizations, this is probably not suitable for high-school students, but it's possible to unify the rule of signs with the Newton polygon via hyperfields in the sense of Krasner arxiv#1811.04966 )

[Johan Commelin]

That was not the kind of variant I was thinking of (-;

[Adam Topaz]

I figured as much :wink:

[Adam Topaz]

What were you thinking of?

[Johan Commelin]

https://en.wikipedia.org/wiki/Descartes%27_rule_of_signs#See_also

[Taylor Belcher]

Thank you!

[Wenda Li]

Some related formalisation in Isabelle: https://www.cl.cam.ac.uk/~wl302/publications/cpp19.pdf, in case you are interested :-)

[Taylor Belcher]

Wenda Li said:

Some related formalisation in Isabelle: https://www.cl.cam.ac.uk/~wl302/publications/cpp19.pdf, in case you are interested :-)

Outstanding! Thank you very much.

[Shing Tak Lam]

I think Alex J. Best had worked on this a bit? https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/What's.20new.20in.20Lean.20maths.3F/near/231121914

[Taylor Belcher]

Shing Tak Lam said:

I think Alex J. Best had worked on this a bit? https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/What's.20new.20in.20Lean.20maths.3F/near/231121914

Thank you for pointing this out

[Riccardo Brasca]

Has anyone done this?

[Johan Commelin]

cc @Alex J. Best I guess

[Eric Rodriguez]

I was looking at this a couple months back, the Isabelle formalisation for the stronger version is really lovely and should be amenable to using in Lean. The one thing I think held me back was the API around polynomials as lists, but I'm happy to work on this with some people

[Eric Rodriguez]

(docs#sign_type was born for this, because I focus far too much on making everything super neat...)

[Riccardo Brasca]

I am just looking for a small project to give to a student, this seems interesting and doable (at least the basic version).

[Riccardo Brasca]

It's getting harder and harder to find good small project...

[Yaël Dillies]

Have you asked @Kevin Buzzard? He has lots spare.

[Kevin Buzzard]

I've been trying to collect basic projects for students! I agree it's getting harder, which is why I've been more careful in keeping track of them. But perhaps this isn't the thread to talk about this.

[Alex J. Best]

I haven't worked on this since, several people have been interested in this (also for students), including @Marc Masdeu also, but I don't know what the status of peoples projects is. Maybe Marc can advise on whether this is a good student project or not!

[Riccardo Brasca]

Ok, thanks! After a little discussion I think we will formalize Kaplanski criterion for being a UFD (and maybe the fact that the power series ring over a PID is a UFD as a corollary).

[Yaël Dillies]

Hasn't @Damiano Testa done (a generalisation of) Kaplanski?

[Riccardo Brasca]

Searching Kaplanski on Zulip only gives stuff about Kaplanski conjecture, that is unrelated. I am talking about a criterion for a ring to be a UFD.

[Bolton Bailey]

I started on this with #14916, but haven't touched it in a while.

[Bolton Bailey]

(Descartes rule of signs)

[Junyan Xu]

A comm-alg project on my list is Krull–Akizuki, which can be used to prove docs#integral_closure.is_dedekind_domain without is_separable

[Damiano Testa]

What I formalized had to do with being a domain, i.e. having no non-zero zero-divisors. I did not get to unique factorization stuff! This was in the context of docs#unique_prods.

[Damiano Testa]

The file counterexamples/zero_divisors_in_add_monoid_algebras.lean is the application.

[Riccardo Brasca]

The theorem I am referrering to is the following: a commutative integral domain R is a UFD if only if every nonzero prime ideal of R contains a prime element.

Kaplanski conjecture is about certains modoid algebras being a domain or not, and I think it's totally unrelated.

[Riccardo Brasca]

Maybe "Kaplanski criterion" is not standard terminology, I don't know.