Is there a substitute for polyrith yet?

Stream: metaprogramming / tactics

[Geoffrey Irving]

I have some degree-5 univariate polynomial inequalities over the rationals (with coefficients with many digits of precision) that I want to prove hold over a particular interval Icc 1 2. My understanding is that polyrith used to do this, but is unavailable now. Is that right? Is there a standard alternative? It seems like grobner does equalities but not inequalities.

[Kevin Buzzard]

You're right that polyrith is now unavailable -- somehow the sage server was overwhelmed (possibly with AI models spamming polyrith calls) so they shut it down. But I don't think it ever used to do inequalities; it was just powered by a groebner basis tactic to prove that elements of polynomial rings were in ideals i.e. to solve equalities in commutative ring theory. Does grind work? (by inequality I mean $\leq$ not $\neq$)

[Alex J. Best]

It should be possible to run polyrith with a local sage install instead

[Kevin Buzzard]

(and note that every call to polyrith also returned a linear_combination X suggestion which would work without the external call)

[Geoffrey Irving]

I tried grind with a simple inequality and no luck, alas:

import Mathlib

lemma pos (x : Real) : 0 ≤ x^2 - 2*x + 1 := by
  grind  — No luck

[Henrik Böving]

grind does not have support for non-linear real arithmetic reasoning. If grind ever manages to solve a non linear equation it's because some more abstract interpretation of the equation (e.g. interpreting x^2 as a single variable y in a linear equation) is solvable using another grind facility.