Gröbner bases

Stream: Is there code for X?

[Antoine Chambert-Loir]

Does mathlib know about Gröbner bases? I'm only interested in the division algorithm with respect to some monomial order (which, actually, I have formalized in the branch branch#ACL/Gröbner) but even that does not seem to exist yet.

[Matthew Ballard]

No, I don't think so.

[Johan Commelin]

@Antoine Chambert-Loir do you want to reason about the algorithm? Or only execute it to get proof certificates? Because the latter can be done via polyrith.

[Antoine Chambert-Loir]

I need the mathematical theorem, for example in my formalization of the combinatorial Nullstellensatz, presently PRed, there is a particular case of the general division result (by polynomials, each of them involving only one of the indeterminates), and that annoyed me.

[Johan Commelin]

Ok, gotcha. In that case, indeed we don't have such a theorem yet.

[Antoine Chambert-Loir]

So it'll be there soon! (Up to the time needed by having PRs incorporated into mathlib...)

[Hagb (Junyu Guo)]

@Antoine Chambert-Loir Oops I think we did some duplicated works. I had a Groebner bases implementation (#general > Formalization of multideg, division, etc. of MvPolynomial ), but I have been too busy to try to refactor it and submit a pull request to Mathlib. I am very sorry about this, and thank you for your work.

[Antoine Chambert-Loir]

I'm sorry about that too. Don't hesitate then to review the code and make remarks. I only formalized the division process as I needed it for some other project. I did not start formalizing the definition of Gröbner bases nor their existence or the Buchberger algorithm.

[Hagb (Junyu Guo)]

Antoine Chambert-Loir said:

Don't hesitate then to review the code and make remarks.

Sorry but I haven't touched Lean for a long time and have become unfamiliar with Lean.

I did not start formalizing the definition of Gröbner bases nor their existence or the Buchberger algorithm.

Free feel to formalize them if you want. (And also feel free to pick anything from my code if it can help. My code probably cannot be compiled without modification on the latest Lean4 though.)
When I get free months later, I would come back to my Gröbner formalization, including Buchberger algorithm and some properties of Gröbner bases, and port stuff based on your definitions, if they haven't been formalized by you or others.

[Hagb (Junyu Guo)]

Before I start to work on it in the future, I will let you know, to avoid potential duplication.

[Hagb (Junyu Guo)]

@Antoine Chambert-Loir I noticed that division has been formalized, while Gröbner bases haven't if I haven't missed it. I just wanted to check if you are working on or plan to work on formalization of Gröbner bases and related theorems. If not, I'd be interested in trying to formalize them.

[Antoine Chambert-Loir]

I am not working on it at the moment — and have too much things on my plate. So feel free to go!

[Hagb (Junyu Guo)]

Antoine Chambert-Loir said:

I am not working on it at the moment — and have too much things on my plate. So feel free to go!

@tsuki and I, in @Lihong Zhi's team at AMSS, are working on Groebner basis on https://github.com/WuProver/groebner_proj, based on MonomialOrder and MonomialOrder.div_set on Mathlib, and we plan to gradually submit pull requests to Mathlib to upstream what we're working on.
Remainder of a MvPolynomial on division of a set of MvPolynomial is defined just like the the one whose existence is proved in MonomialOrder.div_set, but allowing a divisor to be 0, which we consider more convenient when it comes to proprieties about Groebner basis and remainder.
We will be thankful for any reviews, remarks, and suggestions.

[Hyunwoo Lee]

Last semester, I (and also my friends) did a project, implementation of groebner basis and buchberger algorithm in Lean. We are not working on this anymore, but hope that it will be helpful for people who want to implement GB related things in Lean.
https://github.com/Hyun2023/GBLean

[Kevin Buzzard]

Note that I believe the forthcoming grind tactic in core Lean will have Groebner bases, in some form at least.

[Markus Himmel]

grind will employ algorithms based on Groebner bases under the hood, but that shouldn't affect any efforts to study Groebner bases as mathematical objects in mathlib.