Computer algebra system in Lean

Stream: new members

[Nick Mertes]

Is there currently any work towards a computer algebra system library in Lean? For example, I am wondering whether there are currently any tools that would allow me to (symbolically) compute eigenvalues and eigenvectors like what Mathematica does.

[Asei Inoue]

I have a same question. I know polyrith tactic uses sage internally

[Matthew Fairtlough]

I have a similar question and I'm also new to most Lean-specific issues esp. mathlib; so far I understand that there are loads of powerful tactics for simplifying Nat's and other basic types (norm_num, calc etc) and very general tactics for manipulating general elements of rings (linarith, nlinarith, polyrith, ...?) and field_simp for fields (also ...?) and satisfiability solvers but I've seen nothing so far anywhere like what Mathematica provides. I'd love to know if this is on the roadmap for mathlib or other projects. Also would like to understand aesop and why it always seems to be mentioned with the term "magic". Happy to be corrected if any of this is wrong!

[Matthew Fairtlough]

of course theres this https://lean-fro.org/about/roadmap-y2/

[Giulio Caflisch]

I'm new to Lean but I'm used to with CAS like Maxima and Wolfram Mathematica.
I was thinking too about how cool it would be, as you mentioned, to have both CAS like solving&simplification and Formalization in Lean 4.

I considered the dummy example of showing that

noncomputable def a : ℕ → ℝ :=
  fun n ↦ Real.exp (- n^2)

tends to 0 as n goes to infinity via a classic ε-N proof.

When I ask Wolfram Mathematica

Reduce[Abs[Exp[-x^2]]<ε, x, Reals]

I get the result analogous to

∀ (x : ℝ), (((0 < ε ∧ ε < 1) ∧ (x < -√(-Real.log ε) ∨ x > √(-Real.log ε))) ∨ (1 ≤ ε) ) ↔ |Real.exp (- x^2)| < ε

Then one could have a solve tactic (can also be incomplete and that finds just sufficient conditions for solution, or work only on specific bigger domains where things are more algorithmic) that one could use like

have sx ::= solution_with_proof /-...-/ for x : ℝ

instead of the tedious

have sx : /-solution_of_...-/ := by
  --long proof

Then the proof would be way more

lemma a_tendsto_zero :
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, n > N → |a n - 0| < ε := by
  intros ε hε
  simp only [sub_zero]
  simp_rw [a]

  have sx ::= solution_with_proof |Real.exp(- x^2)| < ε for x : ℝ   --adds the hypothesis | sn : ∀ (x : ℝ), (((0 < ε ∧ ε < 1) ∧ (x < -√(-Real.log ε) ∨ x > √(-Real.log ε))) ∨ (1 < ε) ) ↔ |Real.exp (- x^2)| < ε
  /-
  have sx : ∀ (x : ℝ), (((0 < ε ∧ ε < 1) ∧ (x < -√(-Real.log ε) ∨ x > √(-Real.log ε))) ∨ (1 ≤ ε) ) ↔ |Real.exp (- x^2)| < ε := by
    sorry
  -/

  let N := Nat.ceil √(- Real.log ε)
  use N
  intros n hn
  have h := (sx n).mp
  apply h
  by_cases hε' : 1 ≤ ε
  · right
    exact hε'
  · rw [not_le] at hε'
    left
    constructor
    · constructor
      · exact hε
      · exact hε'
    · right
      exact Nat.lt_of_ceil_lt hn -- thanks to Luigi Massacci

That is something going in the direction you mentioned that should be added in the next years in my view.

P.S. Does someone know a theorem that tells

(n : R) > (x :  ℝ) ← n > ceil x

so I can finish my example? : :joy:

[Luigi Massacci]

exact Nat.lt_of_ceil_lt hn

[Heather Macbeth]

@Kim Morrison has been advocating an isolate tactic for some time now. It would "isolate" an expression in a given (in)equality by rearranging the stuff around it onto the other side.

[Heather Macbeth]

In your example you could use it at least three times:

import Mathlib
open Real

notation "a" => fun n : ℕ ↦ exp (- n^2)

lemma a_tendsto_zero :
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, n > N → |a n - 0| < ε := by
  intros ε hε
  dsimp
  use ?t
  intro n hn
  rw [abs_lt]
  constructor
  · have : 0 < exp (-n^2) := by positivity
    linarith
  obtain hε1 | hε1 := lt_or_le 1 ε
  · have : exp (-n^2) ≤ 1 := by
      -- syntax for the next line would be `isolate (n:ℝ) ^ 2`
      rw [exp_le_one_iff, Right.neg_nonpos_iff]
      positivity
    linarith
  -- syntax for the next line would be `isolate n`
  rw [sub_lt_iff_lt_add, ← lt_log_iff_exp_lt (by positivity),
    neg_lt, ← sqrt_lt ?_ (by positivity)]
  · -- THIS IS THE MAIN GOAL: ⊢ √(-log (ε + 0)) < ↑n
    sorry
  · -- syntax for the next line would be `isolate ε`
    rw [Right.nonneg_neg_iff, log_nonpos_iff (by positivity), ← le_sub_iff_add_le]
    linarith

[Heather Macbeth]

So

• isolate (n:ℝ) ^ 2 reduces ⊢ exp (-↑n ^ 2) ≤ 1 to ⊢ 0 ≤ ↑n ^ 2
• isolate n reduces ⊢ exp (-↑n ^ 2) - 0 < ε to ⊢ √(-log (ε + 0)) < ↑n (plus a generated side goal, ⊢ 0 ≤ -log (ε + 0))
• isolate ε reduces 0 ≤ -log (ε + 0) to ε ≤ 1 - 0.

[Philippe Duchon]

So this "isolate" tactic would somehow know which functions are increasing, where they have special values, or which are inverses of each other? (I know nothing about tactic writing, so I have no idea how difficult it would be)

[Heather Macbeth]

@Philippe Duchon If you look at the lemmas I was invoking, you'll see they are all of the form F x ∼ y ↔ x ∼' B, where ∼ and ∼' are (possibly different) relations (and there may be side conditions before the iff), and y is a variable or constant:

#check neg_lt -- `-a < b ↔ -b < a`
#check sub_lt_iff_lt_add -- `a - c < b ↔ a < b + c`
#check le_sub_iff_add_le.symm -- `a + b ≤ c ↔ a ≤ c - b`
#check Right.neg_nonpos_iff -- `-a ≤ 0 ↔ 0 ≤ a`
#check Right.nonneg_neg_iff -- `0 ≤ -a ↔ a ≤ 0`
#check exp_le_one_iff -- `exp x ≤ 1 ↔ x ≤ 0`
#check (lt_log_iff_exp_lt ..).symm -- `exp x < y ↔ x < log y` (side condition `0 < y`)
#check log_nonpos_iff -- `log x ≤ 0 ↔ x ≤ 1` (side condition `0 < x`)

[Heather Macbeth]

The idea would be to tag all such lemmas with an isolate attribute at the place in the library where they are proved:

@[isolate] theorem lt_log_iff_exp_lt ....

storing them with the function F and the relation ∼, then have the tactic look them up as needed for the function and relation which it is presented with. (Side goals can be discharged by e.g. positivity, where possible.)

[Heather Macbeth]

If you know how the gcongr tactic works, it would be a similar model to that.

[Yaël Dillies]

I very much back this idea, but what will the tactic do if eg I ask it to isolate a in a - a ≤ 0? Error hopefully?

[Yaël Dillies]

Actually, I could see a use case for wanting to isolate a term that shows up several times in an expression. Eg in my expansion of y maybe I have a main term x and an error term cos x. Something like y = x + cos x then I might want to isolate x to prove x = y - cos x ≤ y + 1.

[Yaël Dillies]

So maybe the tactic should take in a expression with holes, something like (_ <- this is the hole I want you to isolate) + _ for the example above. Syntax for the distinguished hole TBD.

[Damiano Testa]

Maybe the distinguished hole could be ?_.