Let's say I am an ordinary mathematician who is primarily concerned with proving theorems in algebra, usually with pen and paper. If I was working with finitely presented modules or something I could implement it pretty easy in Sage or Mathematica. However for inherently "infinitary" objects it seems that these are perhaps inadequate. Is it reasonable to try to use Coq as a kind of symbolic computation program to manipulate abstract mathematical objects? I'm not interested in formalizing mathematics for its own sake.

What work has been done in Coq in the way of just like, writing software for manipulating mathematical objects and doing computations something analogous to what can be done in Sage, GAP, Macaulay2 or Mathematica

see for example: https://github.com/coq-community/apery and its paper linked in the README

On the same line of research, you may find the (just started) FRESCO project: https://www.inria.fr/en/erc-consolidator-grant-2020-assia-mahboubi-formalising-foundations-mathematics

Last updated: Oct 05 2023 at 02:01 UTC