Lean and basic CAS computations

Stream: new members

[Rado Kirov]

I am reading Cox - Galois Theory and as is usual for me these days and doing the exercises. I ask myself can these be done in Lean. Some exercises are of the sort "verify the computation" where the computation involves symbolic algebra like
Screenshot 2026-02-02 at 2.39.17 PM.png

I can do this simply in sympy simply by:

a, b, c, d = symbols('a b c d')
x, y, z = symbols('x y z')
p, q = symbols('p q')
monic_cubic = x**3 + b*x**2 + c*x + d
substituted = monic_cubic.subs(x, y - b/3).expand()
collected = collect(substituted, y)
print(f"Collected: {collected}")

Is Lean:
1) currently well-suited for these type of computations (not proofs, I think I know how to prove the result once I have it using ring tactic, etc)
2) if not, is it in the plans / vision for Lean to support this type of computation out of the box or it will remain better suited by CAS in the future.

Personally, I find the vision of using Lean for all mathematical explorations - both computational or proof related very compelling.

[Snir Broshi]

I think that's the purpose of #Computer algebra, I'd also love to see progress made towards replacing sympy

[Kevin Buzzard]

Your book is making a huge meal of that calculation! Anything there is easy to do with ring.

[Kevin Buzzard]

You can do the calculation with ring_nf.

[Rado Kirov]

Agree! It’s a one liner, but doesn’t ring need RHS and LHS to prove? How do I just do the computation?

[Aaron Liu]

you can replace the rhs by sorry and run ring_nf

[Kevin Buzzard]

You are not really using the binomial theorem either, that's a statement about (x+y)^n. For concrete n like 2 and 3 you're just using the ring axioms.

[Kevin Buzzard]

BTW if you're trying to figure out the roots of a cubic then I think we have this in mathlib already

[Rado Kirov]

Aaron Liu said:

you can replace the rhs by sorry and run ring_nf

something like this?

import Mathlib
def f (x b c d: ℂ) := x ^ 3 + b * x ^ 2 + c * x + d

example (x y b c d: ℂ) (h: y = x - b / 3) : f y b c d = sorry := by
  ring_nf

Doesn't spit out p and q

[Aaron Liu]

how about this

import Mathlib
def f (x b c d : ℂ) := x ^ 3 + b * x ^ 2 + c * x + d

example (x y b c d : ℂ) (h : y = x - b / 3) : f y b c d = sorry := by
  rw [h]
  unfold f
  ring_nf

[Rado Kirov]

BTW if you're trying to figure out the roots of a cubic then I think we have this in mathlib already

Good to know, it's not quite what I am looking for. I am just reading the textbook to refresh my math knowledge and trying to do all the exercises on paper (stilling hoping to join your FLT project one day, starting with galois theory and number fields refresher).

But as I am doing that I am always brainstorming how would "modernized" undergraduate math class/textbook look like where all computations and proofs are done in Lean and exercises are sorries to be filled in. Such a modern textbook cannot just say read what's in mathlib, in fact mathlib's definitions and proofs might not be pedagogically appropriate, as they are have to support a lot more usecases and under tighter type-checking time constraints (I assume).

[Rado Kirov]

Aaron Liu said:

how about this

import Mathlib
def f (x b c d : ℂ) := x ^ 3 + b * x ^ 2 + c * x + d

example (x y b c d : ℂ) (h : y = x - b / 3) : f y b c d = sorry := by
  rw [h]
  unfold f
  ring_nf

This works great, thanks! I would have been nice if there was a way to collect the powers of x, but gets me close enough to copy paste from the error. So the final solution to the exercise that says "verify the calculation can be"

import Mathlib
def f (x b c d : ℂ) := x ^ 3 + b * x ^ 2 + c * x + d

noncomputable
def qq (b c d : ℂ) := b * c * (-1 / 3) + b ^ 3 * (2 / 27) + d

noncomputable
def pp (b c : ℂ) := b ^ 2 * (-1 / 3) + c

example (x y b c d : ℂ) (h : y = x - b / 3) : f y b c d = x^3 + (pp b c) * x + (qq b c d) := by
  rw [h]
  unfold f pp qq
  ring_nf