Algebraic computations tutorial

Stream: LftCM22

[Rob Lewis]

You can get a local copy of Heather's tutorial by running in the terminal:

leanproject get https://github.com/hrmacbeth/computations_in_lean

[Rob Lewis]

The HTML pages are at https://hrmacbeth.github.io/computations_in_lean

[Patrick Massot]

This can be abbreviated to

leanproject get hrmacbeth/computations_in_lean

[Anatole Dedecker]

I did part of the beta testing, and I really recommend everyone to try some of the examples

[Patrick Massot]

https://en.wikipedia.org/wiki/Stockholm_syndrome

[Johan Commelin]

@Heather Macbeth Thanks you so much for this fantastic talk! It felt like you time-traveled to us from the future!

[Jake Levinson]

Yes that was very impressive!

[Jake Levinson]

And impressive work by @Abby Goldberg and @Dhruv Bhatia on making the linear_combination and polyrith tactics.

[Matthias Köppe]

@Heather Macbeth Great presentation. Would there be interest to move the conversion from Sage objects to Lean inputs from https://github.com/leanprover-community/mathlib/blob/master/scripts/polyrith_sage_helper.py into Sage?

[Rob Lewis]

This would be an interesting thing to discuss! If it's going to be "official" in that sense we might want to think about a more principled way, but yes, there would be interest

[Rob Lewis]

Also @Matthias Köppe we've also come up with some questions for someone familiar with Sage/Singular Grobner basis computations, if you know much about that/know anyone who does :smile:

[Matthias Köppe]

Sage already has lots of conversions to other systems, implemented via methods such as "_maxima_init_", "_fricas_init_" etc. Lean mathlib would be easy to add.

[Matthias Köppe]

I've opened https://trac.sagemath.org/ticket/34180 to keep track of anything Lean-related in Sage

[Matthias Köppe]

Rob Lewis said:

Also Matthias Köppe we've also come up with some questions for someone familiar with Sage/Singular Grobner basis computations, if you know much about that/know anyone who does :smile:

Can't say that I'm an expert on that. Best to ask in https://groups.google.com/g/sage-support

[Matthias Köppe]

Matthias Köppe said:

Sage already has lots of conversions to other systems, implemented via methods such as "_maxima_init_", "_fricas_init_" etc. Lean mathlib would be easy to add.

I have prepared https://trac.sagemath.org/ticket/34182 to illustrate what this could look like