LeanSage: SageMath integration for Lean

Stream: general

[Oliver Dressler]

LeanSage allows you to call SageMath directly from Lean.

It works by translating a Lean term to SageMath code, calling a sage process locally, then translating the result back.

Here are some examples of its current capabilities:

import LeanSage
open Polynomial

-- By default SageMath is used as an oracle. Inserts `sorry` if successful.
def arithmetic : 2^10 = 1024 := by sage
def trigonometry : Real.sin (Real.pi / 4) = Real.sqrt 2 / 2 := by sage
def complex_analysis : Complex.exp (Complex.I * Real.pi) = -1 := by sage
def linear_algebra : (!![1, 2; 3, 4] : Matrix (Fin 2) (Fin 2) ℝ).det = -2 := by sage
def calculus : deriv (fun x : ℝ => x^3) 2 = 12 := by sage
def integration : ∫ x in (0 : ℝ)..(Real.pi/2), Real.sin x = 1 := by sage
def number_theory : Nat.gcd 48 18 = 6 := by sage
def polynomials : eval 3 (X^2 - 2*X + 1 : ℝ[X]) = 4 := by sage
def quadratic_roots : (X^2 - 4 : ℝ[X]).roots = {-2, 2} := by sage
def set_theory : ({1, 2} : Set ℕ) ∪ {2, 3} = {1, 2, 3} := by sage
def modular_arithmetic : (7 : Fin 12) * (5 : Fin 12) = (11 : Fin 12) := by sage
def prime_check : Nat.Prime (2 ^ 607 - 1) := by sage
def log_monotone (x y : ℝ) (h₁ : 0 < x) (h₂ : x < y) : Real.log x < Real.log y := by sage
def interval_mem : (2 : ℝ) ∈ Set.Ioc 0 2 := by sage
def ideal_mem : (6 : ℤ) ∈ Ideal.span ({2, 3} : Set ℤ) := by sage

-- SageMath can provide witnesses, resulting in valid Lean proofs
def pythagorean_witness : ∃ x : ℕ, x^2 + 12^2 = 13^2 := by sage
def quadratic_root : ∃ x : ℝ, x^2 - 3*x + 2 = 0 := by sage
def rational_solution : ∃ x y : ℚ, 3*x + 5*y = 1 := by sage
def matrix_eigenvalue : ∃ l : ℝ, (!![2, 1; 1, 2] : Matrix (Fin 2) (Fin 2) ℝ).det - l * (!![2, 1; 1, 2] : Matrix (Fin 2) (Fin 2) ℝ).trace + l^2 = 0 := by sage
def complex_root : ∃ z : ℂ, z^2 + 1 = 0 := by sage
def bounded_polynomial_root : ∃ x : ℝ, x^3 - 6*x^2 + 11*x - 6 = 0 ∧ 0 < x ∧ x < 5 := by sage

-- Use the sage% term elaborator to evaluate terms and get a "Try this" suggestion
theorem poly_factorization : (X^2 - 5*X + 6 : ℝ[X]) = sage% (X^2 - 5*X + 6 : ℝ[X]).factor := by grind
theorem poly_integration : ∫ x in (0 : ℝ)..(1), (3*x^2 + 2*x + 1) = sage% ∫ x in (0 : ℝ)..(1), (3*x^2 + 2*x + 1) := by sage

-- SageMath as computation backend
#sage deriv (fun x : ℝ => x^4 - 4*x^3 + 6*x^2 - 4*x + 1) 1
#sage ∫ x in (0 : ℝ)..(Real.pi/4), Real.sin x * Real.cos x
#sage Complex.exp (Complex.I * Real.pi / 3) + Complex.exp (Complex.I * 2 * Real.pi / 3)
#sage eval (Real.pi/4) (X^3 - 3*X + 1 : ℝ[X])
#sage Nat.gcd (Nat.factorial 12) (Nat.factorial 8)
#sage ∫ x in (0 : ℝ)..(1), x^2 * Real.exp x
#sage Matrix.trace ((!![1, 2; 3, 4] : Matrix (Fin 2) (Fin 2) ℝ) ^ 3)
#sage eval (Complex.I) (X^2 + 1 : ℂ[X])
#sage ∃ x y : ℚ, 7*x + 5*y = 1

LeanSage is MIT-licensed and available at:
https://github.com/oOo0oOo/LeanSage/

[Niels Voss]

Woah, this is really cool. To confirm, sage isn't actually producing any proofs, so the sage tactic is more for exploration and prototyping than for ending up in the final proof of a proposition, right?

[Oliver Dressler]

The sage tactic currently only (attempts to) produce a proof for existentials; all existential examples above produce a valid proof.

image.png

[Kim Morrison]

Could you say something about the design of the verification part of how it handles existentials? Is it extensible?

[Oliver Dressler]

Sure, LeanSage currently only attempts proofs for existentials because the witnesses provided by SageMath are relatively easily verifiable in Lean using use.

Essentially existentials are mapped to SageMath solve() calls:

• They are detected based on the Expr here.
• Translated to SageMath solve() or solve_diophantine() calls here

Example SageMath call and result:

∃ z : ℂ, z^2 + 1 = 0 → solve(((var("z")^2) + 1) == 0, [z]) → [z == -I, z == I]

The result (actually MathML not pure string) is then parsed back into an IR.

Then it is attempted to extract a witness from this IR here. Often SageMath returns parametrized solution, in which case it is also attempted to concretize the result. Also we compare the result to the expected type here and attempt to pick and coerce valid solutions (e.g. positive values if ℕ). The proof generation part of the pipeline still has lots of potential for improvements.

The IR is then converted back to a Lean term here.

Finally a (very basic) proof is attempted using:
use <witness>; norm_num in our case use -(Complex.I); norm_num

This is generally extensible e.g. to support more witness types. The existentials were just the lowest hanging fruit here.

[Kim Morrison]

It would be great to have an extensible registration mechanism, so that rather than your hardcoded "if types are all in nat and int, call solve", users could trigger different sage calls dependent on the (lean) predicate, probably also with a specified certificate generating meta program to run after use.

[Oliver Dressler]

Kim Morrison said:

It would be great to have an extensible registration mechanism, so that rather than your hardcoded "if types are all in nat and int, call solve", users could trigger different sage calls dependent on the (lean) predicate, probably also with a specified certificate generating meta program to run after use.

Agreed, I have been thinking about custom extensions of the sage command.
For true flexibility (e.g. enabling polyrith-like functionality) this would work:

structure CustomSageCall where
  sageGen : Expr → MetaM (Option String)
  proofGen : String → MetaM (Option (List String)) -- Plain text and/or MathML input

It would also be possible to use Syntax or pprinted Strings w regex. Or MathAST (my IR) but I am reluctant to force people to use this; its easier but limited.

I'm a bit lost here, any preferences?

[Deleted User 968128]

Great topic for #Machine Learning for Theorem Proving

[Deleted User 968128]

Very cool.

Niels Voss said:

Woah, this is really cool. To confirm, sage isn't actually producing any proofs, so the sage tactic is more for exploration and prototyping than for ending up in the final proof of a proposition, right?

I am now wondering if this is more about exploitation rather than exploration.

[Deleted User 968128]

https://github.com/oOo0oOo/LeanSage/

Quick Overview of the Pipeline

1. Translate Expr to MathAST: Translate a Lean term into an intermediate representation (MathAST).
2. Translate MathAST to SageMath: Convert the MathAST into SageMath (Python) code.
3. Computation: Execute in SageMath process. Retrieve result as MathML.
4. Translate MathML to MathAST: Parse the MathML result back into MathAST.
5. Extract and concretize witnesses: If the result is existential, extract the witnesses and attempt to concretize them to Lean terms.
6. Translate MathAST to Lean string: Convert the MathAST back into a Lean term.
7. Result handling: Depending on context show result, insert sorry, insert proof, or suggest a term.

[Kim Morrison]

What benefit are you getting from MathAST? It seems an expensive (and hard-to-agree upon) intermediate representation.

[Oliver Dressler]

The benefits of MathAST are only practical, it helped a lot to make progress in this project:

• It arose, when translating the results back into a Lean term. I wanted structured data to do transformations on (concretization and witness selection). And honestly it was a bit daunting to manually construct a correct Expr for this, since I didn't need an Expr but just a string representation.
• During this back-translation I also ended up reimplementing a lof the Expr parsing logic to find the witness types.
• Given the various translations between different Syntaxes (Expr, Term, MathML, SageMath), MathAST helps with isolation.
• It allowed to test roundtrips Lean -> MathAST -> Lean, which helped a lot with debugging.
• In a prototype without IR, there was so much brittle string handling during recursive traversals.
• Experimentally, calling the sage process is the bottleneck in the pipeline.

So, MathAST serves to increase modularity, maintainability and reduce code duplication (basically SWE reasons). It could be removed in a huge refactor w many consequences. That's why I would keep it internal.