Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: practice: software

Topic: Computer algebra

Patrick Nicodemus (Jun 08 2025 at 12:24):

How useful are Sage, Mathematica and other computer algebra systems (or symbolic algebra systems) for doing category theory?

I do not know much about computer algebra. Here is my rough stereotyped understanding:

there are computer algebra systems which deal with finitely presented algebraic structures
there are symbolic algebra systems which can deal with abstract, not necessarily finite structures, and they can do things like equational rewriting between words in a group, or integration/differentiation; maybe they can even do conditional rewriting (a = b under hypothesis H where H is something decidable)
there are theorem provers and proof assistants, which are maximally flexible and can encode arbitrary reasoning

I use Rocq to formalize category theory but I'm wondering if there is a less time intensive way to use computers to help me do long computations in category theory.

Evan Patterson (Jun 08 2025 at 12:29):

You might also check out CAP - Categories, Algorithms, and Programming. I haven't tried it yet myself but the system looks quite impressive. It seems to have a focus on additive and abelian categories, though there's also plenty of stuff for ordinary category theory.

Patrick Nicodemus (Jun 08 2025 at 12:30):

Thank you. This is not the first time that GAP has come up here. I recall this conversation - #theory: category theory > software packages for computer-assisted category theory @ 💬

Patrick Nicodemus (Jun 08 2025 at 12:31):

I will check out GAP I guess and try to understand what it can be useful for

Evan Patterson (Jun 08 2025 at 12:35):

Though CAP is written in GAP, from what I understand, it's best understood as its own system.

Jacques Carette (Jun 08 2025 at 13:28):

The "old school" CASes (Maple, Mathematica) are largely useless for CT. Oh, you can program them with what you want, but out of the box, there is nothing.

It would be nice to see the area of "computational category theory" get reborn. With even more types than the original.

Ryan Wisnesky (Jun 08 2025 at 17:48):

When we originally stated building CQL (http://categoricaldata.net) we looked at a bunch of computer algebra systems to power it. But none of them had sufficient automated theorem proving capability to be able to routinely decide word problems in finite presentations. For example, Mathematica's Knuth-Bendix completion algorithm was (is?) from the 90s and simply didn't perform. On the other hand, our survey was ten years ago; perhaps CAS systems have improved.