Groebner Basis Tactics

Stream: general

[Syx Pek]

Is there currently a way to do Groebner Basis in Lean?

[Mario Carneiro]

short answer is no. Long answer is what do you mean?

[Syx Pek]

Ive been thinking of trying to proving geometrical theorems via an algebraic approach. Obviously, I could generate a groebner basis externally and use it as a certificate for theorems, but was wondering is there already work done on making tactics do it directly.

[Reid Barton]

I think the answer is "not as far as anyone here knows".

[Reid Barton]

I'm guessing that doing the computations in Lean would be a lot slower (for now) and a lot more work and, if you can have an external tool give you a certificate that can be checked efficiently, doesn't really have any advantages besides not depending on an external tool.

[Reid Barton]

@Syx Pek on the other hand much of the work that would be required might be useful for implementing other tactics, as well.

[Kevin Buzzard]

We only got polynomials in one variable about a month ago, I think groebner bases are some time off yet.

[Bolton Bailey]

The tactic that calls Sage to solve Gröbner basis problems is related enough to some of my work that I'd like to cite it. To the contributors behind that tactic have a preferred way of citing it?

[Bolton Bailey]

@Heather Macbeth

[Bolton Bailey]

@Rob Lewis

[Newell Jensen]

@Dhruv Bhatia

[Heather Macbeth]

Dhruv is the author, and he was supervised by Rob; I'll let them get back to you on this.