Loops with Abelian Inner Mapping Groups

The Aim of AIM

• If Q is a loop with commuting inner mappings ...
  • Is Q modulo its center a group?
  • Is Q modulo its nucleus an abelian group?
• True for several varieties of loops
• I'm just a logician who trusts mathematicians

Using ATP

• Done using Prover9
• Requires sophisticated ATP, e.g., proof sketches
• Proofs are very long (viewed with IDV)
• Often no higher level human proofs available

Two Mathematicians and a Computer Scientist Walk into a Bar

• Michael Kinyon
• Petr Vojtěchovský
• Robert Veroff