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.

[Hagb (Junyu Guo)]

Hagb (Junyu Guo) said:

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.

We have proved Buchberger's criterion over $k[X]$ where $k$ is a field, as well as other definitions and theorems it needs. We plan to clean up our code and submit them to mathlib4. We also plan to try to verify the Buchberger's algorithm in the near future.

[Hagb (Junyu Guo)]

Kevin Buzzard said:

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

May I ask what tactic grindis and how it will use Groebner basis? I failed to find public document about it.
We planned to make some tactics for computations about multivariate polynomial division and Groebner basis over $k[X]$ (if new tactics are necessary for them), but we'd like to avoid reinventing the wheel.

[Markus Himmel]

grind is a currently unreleased general-purpose proof automation system. It contains various submodules to solve goals of various kinds. One of the submodules is a decision procedure for certain concrete statements in commutative rings (see here for some examples). This decision procedure happens to use Gröbner bases (among other things) under the hood. This is an implementation detail. If tomorrow there is a paper that presents a better decision procedure, then grind might throw away the Gröbner bases and switch to the new procedure.

[Kevin Buzzard]

In other words, we still definitely want Groebner bases in mathlib, this is not what grind is doing :-)

[Lihong Zhi]

Junyu Guo and Hao Shen are doing a great job building Groebner bases in Lean.

[Mauricio Barba da Costa]

Will the grind tactic allow for proving the existence of a solution to a polynomial equation? I.e. by showing that 1 is not in the Grobner basis?

[Kevin Buzzard]

Why not try it? It's all been merged.

[Mauricio Barba da Costa]

Here are two approaches I've tried, but neither works with grind.

theorem test1 :
  ∃ x₁ x₂ : ℝ, (x₁ + x₂ = 1) := by
  grind

theorem test2 (x₁ x₂ : ℝ) :
  ¬ ((x₁ + x₂ = 1) → 1 = 0) := by
  grind

I guess I'm wondering if there is a (possibly even hacky) way of writing a theorem like this that would be amenable to automated proving with grind. If not, I'm curious if there is an intention to add this feature in the future.

[Johan Commelin]

fwiw, the second theorem is false.

[Mauricio Barba da Costa]

Thanks for pointing that out. I think this is the corrected version. It also doesn't work with grind:

theorem test2 :
  ¬ (∀ x₁ x₂ : ℝ, (x₁ + x₂ = 1) → 1 = 0) := by
  grind

[Kenny Lau]

why are you writing 1=0? that's how a logician would say contradiction, but in Lean it's just called False

[Mauricio Barba da Costa]

I'm just using it as an example to show that grind can't show that a system of polynomial constraints admits a solution, even though such a feature should be possible with a Grobner basis solver. 1=0 is the contradiction that a Grobner basis algorithm would arrive at.

[Hagb (Junyu Guo)]

Hagb (Junyu Guo) said:

Hagb (Junyu Guo) said:

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.

We have proved Buchberger's criterion over $k[X]$ where $k$ is a field, as well as other definitions and theorems it needs. We plan to clean up our code and submit them to mathlib4. We also plan to try to verify the Buchberger's algorithm in the near future.

Nearly all of our lemmas dependent on only definitions currently in mathlib4 have been submitted and merged into Mathlib. We're now upstreamizing our main definitions and theorems via PR #29203. We appreciate any review and suggestion.

edit: independent of our new definitions -> dependent on only definitions currently in mathlib4; quote more deeply.

[Kim Morrison]

@Hagb (Junyu Guo), that PR depends on #26039, which I see is marked awaiting-author, but a cursory look suggests that you've responded to the last round of comments. Did you mean to remove awaiting-author so this can be reviewed further?

[Hagb (Junyu Guo)]

Kim Morrison said:

Hagb (Junyu Guo), that PR depends on #26039, which I see is marked awaiting-author, but a cursory look suggests that you've responded to the last round of comments. Did you mean to remove awaiting-author so this can be reviewed further?

Did you mean to remove awaiting-author so this can be reviewed further?

Okay. I didn't resolved all conversation at that time (since I was waiting for response in some of them), so I didn't remove this tag.