On Tue, May 3, 2022 at 1:51 AM Dima Pasechnik <d...@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.z...@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@gap-system.org > > https://mail.gap-system.org/mailman/listinfo/forum _______________________________________________ Forum mailing list Forum@gap-system.org https://mail.gap-system.org/mailman/listinfo/forum
