Lean CAS

Stream: general

[Riyaz Ahuja]

A bit of an idle thought, but I've been playing with mathematica and maple lately, and was curious if there is any work being/been done on integrating CAS systems with lean?

I'm not too sure what such an integration would look like, but I'd imagine being even just being able to offload large sequences of algebraic computations would be very useful for theorem proving. Though, integrating that with lean in a way that allows the symbolic/numerical computations to still be provable and used by theorems seems like it'd be difficult.

[Luigi Massacci]

You can look at the polyrith tactic which calls Sage for an example, and is a heavily used tactic too. Otherwise, there was some work integrating with Oscar #general > Lean Oscar Interface , as well as this thread discussing approaches for integration with Sage: #general > What should Sage look like in Lean?

[Luigi Massacci]

it’s definitely a worthwhile goal