Stream: Coq users

Topic: Group theory related theorem proving by coq.


view this post on Zulip Hongyi Zhao (May 04 2022 at 14:36):

Can I do the group theory related theorem proving, say, Rearrangement
Theorem [1], by coq?

[1] https://mathworld.wolfram.com/RearrangementTheorem.html

Regards
HZ

view this post on Zulip Karl Palmskog (May 04 2022 at 14:40):

if you're content with finite groups, I'd recommend looking at the encoding of finite groups in MathComp, in particular fingroup.v. See also the math-comp users stream


Last updated: Feb 04 2023 at 21:02 UTC