Kernel-checked Lean 4 proof that no infinite simple paramedial quasigroups exist (Loops '03 open problem).
theorem-proving abstract-algebra mathlib quasigroup universal-algebra nonassociative-algebra lean4 formal-proof open-problem loop-theory paramedial
-
Updated
Jul 23, 2026 - Lean