integrate with other math software

Stream: new members

[stark]

Is it possible to integrate lean and other math software like sage and geogebra to enhance its ability of calculation and geometry plotting ?

[Jireh Loreaux]

There is some interaction between Lean and computer algebra systems. For example, the polyrith tactic outsources the Gröbner basis calculation to sage in order to produce a certificate that Lean can check quickly. What exactly are you looking for?

[stark]

For example, I want to add a widget of geogebra, plotting on it and transfer data to lean and prove the geometry theorem in lean.

Jireh Loreaux said:

There is some interaction between Lean and computer algebra systems. For example, the polyrith tactic outsources the Gröbner basis calculation to sage in order to produce a certificate that Lean can check quickly. What exactly are you looking for?

[Jireh Loreaux]

What data exactly do you imagine being transferred? Can you provide a simplified example?