[GAP Forum] Group theory related theorem proving by GAP.

[Hongyi Zhao]

On Tue, May 3, 2022 at 1:51 AM Dima Pasechnik <dima at sagemath.org> wrote:
>
> On Sat, Apr 30, 2022 at 11:25:52PM +0800, Hongyi Zhao wrote:
> > Can I do the group theory related theorem proving, say, Rearrangement
> > Theorem [1], by GAP.
>
> no, GAP, or in fact any mainstream or not so mainstream CAS, don't do theorem proving.
> One needs a proof assistant for this (Coq, Agda, Lean, etc)

Thank you for telling me this fact. Here are some related resources:

https://github.com/leanprover/lean4
https://github.com/agda/agda
https://github.com/idris-lang

https://stackoverflow.com/questions/29905344/a-good-way-to-formalize-groups-in-coq
https://stackoverflow.com/questions/11531589/difference-between-z3-and-coq
https://github.com/WhatisRT/WhatisRT.github.io
https://whatisrt.github.io/dependent-types/2020/02/18/agda-vs-coq-vs-idris.html

https://github.com/coq-community/coq-100-theorems
https://madiot.fr/coq100/

https://github.com/coq-community/fourcolor
https://github.com/coq-contribs/group-theory


> HTH
> Dima

Yours,
Hongsheng

>
> >
> > [1] https://mathworld.wolfram.com/RearrangementTheorem.html
> >
> > Regards
> > --
> > Assoc. Prof. Hongsheng Zhao <hongyi.zhao at gmail.com>
> > Theory and Simulation of Materials
> > Hebei Vocational University of Technology and Engineering
> > No. 473, Quannan West Street, Xindu District, Xingtai, Hebei province
> >
> > _______________________________________________
> > Forum mailing list
> > Forum at gap-system.org
> > https://mail.gap-system.org/mailman/listinfo/forum