Commit 2025-09-25 14:17 ee0f6ec0

chore: remove defunct polyrith tactic (#29547) In my understanding, the public Sage server that polyrith relies on is down and never going to come back, and hence the polyrith code is dead. There are a bunch of viable options for restoring this, e.g. running Sage locally, running our own Sage server, moving to a different external CAS, implementing Grobner bases in a way that produces nullstellensatz certificates (including by modifying the grind implementation). But none of these exist at the moment, so this code in Mathlib is not of any use. It can immediately be restored from history if someone wants to implement one of these solutions. In the meantime, one can also use grobner (which calls the Grobner module in grind) to close the goal without a source code certificate.