News for hackers. Stuff that matters.

A comment on Mathematicians welcome computer-assisted proof in ‘grand unification’ theory. Parent comment

Re:Mathematicians welcome computer-assisted proof in ‘grand ... by Ericson2314 on Sunday June 20, 2021 @07:46PM (#27574838)
Your concerns make sense in general, but I have hard time understanding them for would-be subgroups. I would think the "explicit function" would be the easy part. The hard pat is annoyance of finding a "syntactic" representation of the subgroup and proving it's a group (closed) in its own right.

In any event, Lean's reputation is that it goes the extra mile for "regular" mathematicians. It probably has something nicer for this just like it does for quotiented types.

[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by Jweb_Guru on Monday June 21, 2021 @01:16PM (#27581237)
Nope, proving something is a group doesn't usually run into foundational concerns (at least if you use setoid equality). But finding a function exhibiting a homomorphism can unless you use a functional relation instead (but then you lose most of the nice benefits of using this version of the definition in the first place).
[ Parent | on HN ]