Macaulay2 and lean

Stream: new members

[Michael Stillman]

Hi everyone, I'm Mike Stillman, an author of the Macaulay2 computer algebra system. I am interested in lean4, and possibly connections between lean and Macaulay2.

[Anton L.]

I just wanted to introduce myself as well --- Anton Leykin.
In far (or near) future, I'm interested in creating a Macaulay2 (M2) interface to lean in order to formalize results of certain computations. It would be interesting to see how large the intersection of the M2 and lean communities is. (So far we talked to @Damiano Testa and @Matthew Ballard.)

[Mario Carneiro]

Great, you'll want to check out #Computer algebra (which I think hasn't had much activity yet but maybe will see some more motion now). This has been a topic of random discussions for many years but it hasn't really reached critical mass yet.

[Mario Carneiro]

From our side I think we want to have either connections to the system to get certificates for come kinds of formal computations (an example of this is that we currently use sagemath to compute Gröbner bases for the polyrith tactic), or to get CAS algorithms reimplemented in a proof producing or verified-correct way in Lean (which is difficult to do without contacts who work on the unverified version of the algorithm).