LeanM2

Stream: general

[Riyaz Ahuja]

Hi everyone, I've been working for the last few weeks on a Lean-Macaulay2 interface. The idea is to be able to get all the powerful computational abilities of M2 while also building proof certificates/witnesses that allow for these computational results to be used in real Lean proofs.

Towards this, I have made a prototype (github) that extends polyrith. Namely, it is a tactic that can solve ideal membership questions using Grobner bases, but instead of being restricted to only polynomials in $\mathbb{Q}$, it can work over $\mathbb{Z}$,$\mathbb{Q}$,$\mathbb{R}$,$\mathbb{C}$, $\mathbb{Z}$ mod p, polynomial rings over the aforementioned, and quotient rings over the aforementioned. Moreover, these are all just special cases to show a more general Lean-M2 lifting system.

This is still an early prototype, and I intend to keep developing this to adopt more and more of M2's types and functions into Lean. However, towards this, I wanted to first survey the general community to first see what kinds of use cases people would like to see of M2/CAS tools in Lean, and what you all might find the most useful. Let me know where you think this might be useful!

[Kevin Buzzard]

Can Macaulay2 compute group cohomology for finite groups and finite modules and provide a witness concrete enough for lean to be able to reproduce the proof?

[Luigi Massacci]

Computing integral bases for rings of integers in number fields (and stuff that follows, such as computing ideal norms) would be cool. Great work in any case!

[Kevin Buzzard]

The problem with these suggestions is that lean won't be able to work with just the answer that M2 gives, there needs to be a certificate too so that lean's kernel can verify the proofs

[Riyaz Ahuja]

Kevin Buzzard said:

Can Macaulay2 compute group cohomology for finite groups and finite modules and provide a witness concrete enough for lean to be able to reproduce the proof?

It seems that M2 supports cohomology of modules and sheaves (see: modules, sheaves, table), but I'm not too sure on groups (probably possible in an ad-hoc way using the AssociativeAlgebras package to get the group algebra?). I think that GAP(HAP) is a better CAS for this kind of group cohomology stuff -- as it is explicitly designed for that application. The core trick behind LeanM2 though is the type bridge, which basically just binds the types of Macaulay2 to their Mathlib counterparts, and is rather easily extended to other languages and their syntax, such as that of GAP.

So in either case, as you said, getting a sufficiently explicit witness for the proof is the key question to answer if this is something that LeanM2 could feasibly add. What kind of witness does Mathlib expect for these cohomology questions?

[Riyaz Ahuja]

Luigi Massacci said:

Computing integral bases for rings of integers in number fields (and stuff that follows, such as computing ideal norms) would be cool. Great work in any case!

It seems that the RationalPoints2 package has a lot of tools for exactly this (calculate integral basis, get discriminant, get Hermite NF of (fractional) ideals, and use that to get ideal norms).

Also, since M2 provides the minimal polynomial, proving the basis is valid in Lean should just come down to showing integrality of elements, linear independence, and span which should be able to be automatically proven using the min poly, matrix rank, and discriminant? I don't do much algebraic number theory, so I'm not too sure how hard it would be to build this certificate, but it doesn't seem impossible.

[Riyaz Ahuja]

Of course these (+ all other ideas of applications) are still in the future, but I do believe that if the core type bridge is robust enough, the challenge of porting over functions from M2 (or GAP, Sage, or any other CAS) will just come down to convincing Lean that the CAS is correct with well constructed certificates. Of course, there are large classes of problems where that convincing is rather unfeasible, but I think that there are equally large classes where the computation of some object is both useful and very diffcult, but once you have a value, the confirmation of correctness is far simpler than the actual computation. It is the latter type that LeanM2 hopes to help solve.

[Kevin Buzzard]

Oh if group cohomology is not there then just replace my question with module or sheaf cohomology. I was just basically trying to think of something fancy which both systems have because if one day we can say "mathlib has formally verified sheaf cohomology calculations backed up by M2" then it's just a random cool thing which would be completely new.

As for integers of number fields, you haven't said enough to convince me yet. Proving that the basis is integral should be fine but how does one prove that the discriminant of the number field is what M2 says it is? IIRC there was some talk a while ago about getting Lean glued together with LMFDB and I could imagine that M2 could play a role here. Was it Andrew Sutherland who posted about this a few months ago? On mobile so search is crippled for me rn

[Riyaz Ahuja]

Yeah getting module/sheaf cohomology would be cool for sure, it just really depends on if we can convert some M2 output into a valid Mathlib construction of a cohomology. Building that witness will definitely be the hardest part there.

With the number field stuff, maybe just use the fact that the discriminant is the determinant of the trace matrix? M2 can compute the trace matrix, and having lean prove that it is indeed a trace matrix shouldn't be impossible. Then we just have lean compute the determinant of this/confirm that M2 can correctly calculate determinant perhaps? It'd be a little annoying to implement, but it would also have the added benefit of confirming that M2 can compute determinants and discriminants explicitly, which would also probably be nice to have as a tactic.

[Riyaz Ahuja]

^ Not sure how difficult the mathlib api would be for these computation confirmations, but it might be a way forward? Will have to experiment more.

[Kevin Buzzard]

Computing ring of integers: isn't this circular? You're saying "you can prove the ring of integers is what we say by using the discriminant and you can prove the discriminant is what we say by using the ring of integers"?

[Patrick Massot]

Do you know about https://dl.acm.org/doi/10.1145/3703595.3705874 ?

[Kevin Buzzard]

No I did not! (or I did but forgot). Yes this is (round 2 or 4 algorithms) is the correct thing to do. Excellent!

[Matthias Köppe]

Since lean-m2 is already using Python, there may be interest in https://pypi.org/project/passagemath-macaulay2/ -- a pip-installable Python interface to M2 which brings a prebuilt M2 in its binary wheels

[Alain Chavarri Villarello]

This looks like a really cool project @Riyaz Ahuja !

Regarding integral basis verification, in our paper (with @Anne Baanen and @Sander Dahmen), which @Patrick Massot kindly linked, our approach was to define a local certificate of maximality based on the Pohst-Zassenhaus theorem, which underlies the Round 2 algorithm. We can actually avoid discriminant computations entirely in Lean (which would require either computing the trace matrix or the matrix of embeddings and its determinant, or, alternatively, the discriminant of the defining polynomial $f$) by instead just proving to Lean the equality $a*f + b*f’ = n$ for some polynomials $a$ and $b$ and non-zero integer $n$, and showing $p$-maximality for the primes $p$ dividing $n$ (if $p$ does not divide $n$, then $\mathbb{Z}[\alpha]$ is automatically $p$-maximal by Dedekind criterion). 

Nonetheless, we were still interested in computing discriminants of number fields, so we ended up defining resultants and discriminants of polynomials in Lean and are currently working on computing those efficiently. 

Regarding CAS-Lean integration, I think having standard linear algebra tools over fields and, more generally, PIDs would be really useful. For instance: efficiently verifying the rank of a matrix or the Hermite normal form, determinant, characteristic polynomial etc.