Patrick Nicodemus (May 23 2022 at 05:29): Patrick Nicodemus (May 23 2022 at 05:29):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.
Patrick Nicodemus (May 23 2022 at 05:30):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
Karl Palmskog (May 23 2022 at 08:23):see for example: https://github.com/coq-community/apery and its paper linked in the README
Enrico Tassi (May 23 2022 at 08:31):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