computer algebra and lean

Stream: general

[Laurent Bartholdi]

After finishing @Kevin Buzzard 's course up to and including group cohomology, it dawned on me that there are strong connections between theorem proving à la lean (which I'm getting only now a bit familiar with) and computer algebra systems such as GAP and Magma (which I know much better).

The link I see is through "interfaces": while Kevin defines, say, H^2(G,M) as a set, and then forces on it an abelian group structure, induced maps coming from morphisms M->N or G->H, and properties such as exactness, a GAP package would define a constructor H^2(G,M), with properties "IsAdditiveGroup", methods producing induced maps, and would exploit exactness by giving attributes to these induced maps so that the kernel of one is automatically deduced from the image of another.

I wonder whether there is some sense in making the connection between provers and computer algebra systems more explicit, and whether there are already efforts in this direction?

I can imagine that, in some cases, the computer algebra system could contribute something valuable to the prover: e.g. if the CAS proved that a given finitely presented group is trivial, it could feed the Tietze transformations back into a prover for certification. If, as I groked from Kevin's classes, the underlying interfaces are actually very close (with the CAS on the "computing explicitly" side and the prover on the "apply axioms" side of the interface), it may pay off to have them actually match.

Comments of course welcome!

[Sebastien Gouezel]

If you have some time to spare, I can only encourage you to read @Assia Mahboubi 's HDR memoir https://tel.archives-ouvertes.fr/tel-03107626/file/memoir_with_cover.pdf, which is a wonderful read and advocates among many things this idea that interactions between CAS and proof assistants is a very worthwhile goal.

[Sebastien Gouezel]

(Have a look at Listing 5.1 on Page 77 if you're curious and brave enough)

[Floris van Doorn]

@Rob Lewis and @Minchao Wu have a paper on connection Lean to Mathematica: https://arxiv.org/abs/2101.07758v1

[Johan Commelin]

@Sebastien Gouezel Thanks for the link! That example on p77 is really terrifying.

[Kevin Buzzard]

@Laurent Bartholdi Thanks very much for going through my course! It is going to become an undergraduate course next year -- this was a trial run. Let me know if you have any comments!

PS Listing 5.1 is indeed terrifying. I remember reading in Assia's zeta(3) paper about the dangers of creative telescoping (mentioned in 3.6).

[Scott Morrison]

Bridges are great, and we should have more of them! A big obstacle is setting things up in a way that you can generate a Lean-only proof certificate from your interaction with the bridge, so that the software at the other end of the bridge isn't required for every recompilation. There's generally a problem that we have no intermediate layer between .lean files and .olean files, where we can cache large automatically generated proof objects.

[Scott Morrison]

And besides bridges, there's no particular reason why mathlib can't itself become more like a CAS. This is mostly a matter of writing tactics, in fact. (e.g. it's crazy we don't have expand and factor, or factor_integer, etc. as tactics already). Doing so in an organised, principled way would be great, but doing it at all would be even better.

[Scott Morrison]

See #2730 for an old discussion in this direction.