← All papers
Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups
cs.LO
Jan 1, 2025 · v1
TL;DR
Formalizes presentations of graded unipotent Chevalley groups in Lean 4.
Abstract
This paper formalizes in Lean 4 presentations of graded unipotent subgroups of Chevalley groups, verifying that certain algebraic relations hold within these groups. The work combines computational algebra techniques with formal verification to establish correctness of group presentations that arise in the study of algebraic groups.
Problem
Presentations of graded unipotent subgroups of Chevalley groups involve complex algebraic relations whose correctness is difficult to verify by hand.
Approach
The authors formalize in Lean 4 presentations of graded unipotent subgroups of Chevalley groups, combining computational algebra techniques with formal verification to establish that certain algebraic relations hold within these groups.
Results
The formalization verifies the correctness of group presentations arising in the study of algebraic groups, providing machine-checked guarantees for results that combine computational and algebraic reasoning.