BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Michael Kinyon (University of Denver\, USA) DTSTART:20260629T150000Z DTEND:20260629T160000Z DTSTAMP:20260714T041110Z UID:ENAAS/185 DESCRIPTION:Title: The Structure of Left Cheban Loops\nby Michael Kinyon (University of D enver\, USA) as part of European Non-Associative Algebra Seminar\n\n\nAbst ract\nOne natural way to study nonassociative loops is to consider those s atisfying identities generalizing associativity. For example\, the most we ll-known class are Moufang loops\, which can be defined as those satisfyin g the identity $(xy)(zx)=x((yz)x)$ or other equivalent identities. In 1976 and 1980\, A.M. Cheban studied 19 identities of a certain prescribed type . Among these were $x((xy)z) = (yx)(xz)$\, $(z(yx))x = (zx)(xy)$\, and $x ((xy)z) = (y(zx))x$. These are now known as the left Cheban\, right Cheban \, and Cheban identities\, respectively. Cheban gave some examples and sho wed that a loop satisfies the first two identities if and only if it satis fies the third. There matters stood until 2010 when J.D. Phillips and V. S hcherbacov published a short paper examining the structure of Cheban loops \, with all proofs given by the automated theorem prover Prover9.\nBy a mi x of human and automated reasoning\, Ale\\v{s} Dr\\'{a}pal and I have stud ied left Cheban loops in detail and now have a good understanding of their structure. In this talk I will describe that structure. Since an audience member outside of loop theory (and many within loop theory!) will probabl y not care very much\, I will also use the opportunity to talk about how m uch responsibility we do or do not have to ``humanize'' proofs generated b y automated theorem provers.\n LOCATION:https://researchseminars.org/talk/ENAAS/185/ END:VEVENT END:VCALENDAR