Module 5 · Lesson 6

polyrith

Automatically find polynomial certificates for algebraic goals.polyrith uses external solvers to discover proofs that would be tedious to write by hand.

❗

polyrith requires Mathlib and an internet connection to query external polynomial solvers. Add import Mathlib.Tactic.Polyrith.

Basic Usage

lean

1import Mathlib.Tactic.Polyrith
2
3-- polyrith solves polynomial equations
4example (x y : ℚ) (h1 : x + y = 3) (h2 : x - y = 1) : x = 2 := by
5  polyrith
6
7example (a b c : ℚ) (h1 : a + b + c = 0) (h2 : a*b + b*c + c*a = 0) : 
8    a^2 + b^2 + c^2 = 0 := by
9  polyrith

Key Takeaway

polyrith finds polynomial combinations of hypotheses that prove the goal. It's like a super-poweredring that also uses your hypotheses.

How polyrith Works

lean

1import Mathlib.Tactic.Polyrith
2
3-- polyrith finds coefficients c₁, c₂, ... such that:
4-- c₁ * h₁ + c₂ * h₂ + ... = goal
5
6-- Example: Prove x = 2 from x + y = 3 and x - y = 1
7-- Solution: (1/2)(x + y - 3) + (1/2)(x - y - 1) = x - 2
8example (x y : ℚ) (h1 : x + y = 3) (h2 : x - y = 1) : x = 2 := by
9  polyrith
10  -- polyrith discovers: linear_combination (1/2) * h1 + (1/2) * h2

polyrith Output

lean

1import Mathlib.Tactic.Polyrith
2
3-- polyrith suggests a linear_combination proof
4example (a b : ℚ) (h1 : a + b = 5) (h2 : a - b = 1) : a = 3 := by
5  polyrith
6  -- Try this: linear_combination (1/2) * h1 + (1/2) * h2
7
8-- You can use the suggestion directly:
9example (a b : ℚ) (h1 : a + b = 5) (h2 : a - b = 1) : a = 3 := by
10  linear_combination (1/2) * h1 + (1/2) * h2

💡

Use polyrith to discover proofs, then replace it with linear_combination for faster compilation (no network call).

Polynomial Goals

lean

1import Mathlib.Tactic.Polyrith
2
3-- polyrith handles genuinely polynomial (nonlinear) problems
4example (x y : ℚ) (h1 : x^2 + y^2 = 1) (h2 : x + y = 1) : 
5    x * y = 0 := by
6  polyrith
7
8-- It can find complex polynomial combinations
9example (a b : ℚ) (h : a^2 = b^2) : (a - b) * (a + b) = 0 := by
10  polyrith

Deep Dive: The Polynomial Method

polyrith implements the polynomial method:

Converts goal and hypotheses to polynomial equations
Queries a Groebner basis solver or SOS solver
The solver finds polynomial coefficients (if they exist)
Constructs a Lean proof using these coefficients

This is complete for polynomial algebra: if a goal follows from hypotheses by polynomial reasoning, polyrith will find it.

linear_combination

lean

1import Mathlib.Tactic.LinearCombination
2
3-- linear_combination applies a known combination
4example (x y : ℚ) (h1 : 2*x + y = 7) (h2 : x + 3*y = 11) : 
5    x = 2 := by
6  linear_combination (3 * h1 - h2) / 5
7
8-- You specify the coefficients; it verifies and applies them
9example (a b c : ℚ) (h1 : a = b + 1) (h2 : b = c + 1) : 
10    a = c + 2 := by
11  linear_combination h1 + h2

When polyrith Helps

lean

1import Mathlib.Tactic.Polyrith
2
3-- 1. Systems of equations
4example (x y z : ℚ) 
5    (h1 : x + y + z = 6) 
6    (h2 : x + 2*y + 3*z = 14) 
7    (h3 : x + 4*y + 9*z = 36) : 
8    x = 1 := by
9  polyrith
10
11-- 2. Derived algebraic facts
12example (a b : ℚ) (h : a + b = 0) : a^3 + b^3 = -3*a*b*(a + b) := by
13  polyrith  -- Uses h to show a^3 + b^3 = 0 = -3ab*0
14
15-- 3. Verification of formulas
16example (x : ℚ) : (x + 1)^3 - (x - 1)^3 = 6*x^2 + 2 := by
17  ring  -- ring can do this too!

Limitations

lean

1import Mathlib.Tactic.Polyrith
2
3-- polyrith doesn't handle:
4
5-- 1. Inequalities (use linarith, nlinarith)
6-- example (x : ℚ) (h : x > 0) : x^2 > 0 := by polyrith  -- Fails
7
8-- 2. Non-polynomial functions
9-- example (x : ℝ) : sin(x)^2 + cos(x)^2 = 1 := by polyrith  -- Fails
10
11-- 3. May timeout on complex goals
12-- 4. Requires network connection

Real-World Examples

Vieta's Formulas

lean

1import Mathlib.Tactic.Polyrith
2
3-- If r, s are roots of x^2 - px + q = 0
4-- Then r + s = p and rs = q
5theorem vieta (r s p q : ℚ) 
6    (h1 : r^2 - p*r + q = 0) 
7    (h2 : s^2 - p*s + q = 0)
8    (h3 : r + s = p) : 
9    r * s = q := by
10  polyrith

Identity Verification

lean

1import Mathlib.Tactic.Polyrith
2
3-- Sophie Germain identity with constraint
4example (a b : ℚ) (h : a^4 + 4*b^4 = 0) (hb : b = 0) : a = 0 := by
5  polyrith

nlinarith Next: rcases & obtain