Stream: Coq users

Topic: Coq as symbolic algebra or symbolic computation program


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 23 2022 at 08:23):

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

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC