Zulip Chat Archive

Stream: LftCM22

Topic: Algebraic computations tutorial


Rob Lewis (Jul 12 2022 at 19:35):

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 (Jul 12 2022 at 19:35):

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

Patrick Massot (Jul 12 2022 at 19:36):

This can be abbreviated to

leanproject get hrmacbeth/computations_in_lean

Anatole Dedecker (Jul 12 2022 at 19:55):

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

Patrick Massot (Jul 12 2022 at 19:55):

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

Johan Commelin (Jul 12 2022 at 20:51):

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

Jake Levinson (Jul 12 2022 at 21:11):

Yes that was very impressive!

Jake Levinson (Jul 12 2022 at 21:13):

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

Matthias Köppe (Jul 13 2022 at 21:01):

@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 (Jul 13 2022 at 21:16):

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 (Jul 13 2022 at 21:26):

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 (Jul 13 2022 at 21:31):

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 (Jul 13 2022 at 21:32):

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

Matthias Köppe (Jul 13 2022 at 21:33):

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 (Jul 15 2022 at 17:00):

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


Last updated: Dec 20 2023 at 11:08 UTC