AIM Status

February 2022

AIM Loops (clause representation)

```formulas(assumptions).

% loop axioms
1 * x = x.
x * 1 = x.
x \ (x * y) = y.
x * (x \ y) = y.
(x * y) / y = x.
(x / y) * y = x.

% associator (right associated * a = left associated)
(x * (y * z)) \ ((x * y) * z) = a(x,y,z) # label("associator").

% commutator ( (x * y) * K(y,x) = y * x )
(x * y) \ (y * x) = K(y,x) # label("commutator").

% inner mappings
(y * x) \ (y * (x * u)) = L(u,x,y).
((u * x) * y) / (x * y) = R(u,x,y).
x \ (u * x) = T(u,x).

% abelian inner mapping group
T(T(u,x),y) = T(T(u,y),x).
T(L(u,x,y),z) = L(T(u,z),x,y).
T(R(u,x,y),z) = R(T(u,z),x,y).
L(R(u,x,y),z,w) = R(L(u,z,w),x,y).
L(L(u,x,y),z,w) = L(L(u,z,w),x,y).
R(R(u,x,y),z,w) = R(R(u,z,w),x,y).

end_of_list.
```

Weak AIM Conjecture

AIM loops are nilpotent of class 3.

Status:

• Proved with a high-level mathematical argument.

• Challenge: Prove with Prover9.

• Status of 32 goals sufficient to prove that AIM loops are nilpotent of class 3.

• the 8 having > 1 occurrence of K are lemmas
(in, out, pf, xml)

• nil3 15 => the remaining 14 of 15 having exactly 1 occurrence of K
(in, out, pf, xml)

• aK1 + nil3 24 => the remaining 8/32 nil3 clauses having 0 occurrences of K.
(in, out, pf, xml)

• Since aK1 trivially => nil3 15, it follows that aK1 + nil3 24 => nilpotency class 3.

Strong AIM Conjecture

```formulas(goals).

% aK (or "single-a") goals
K(a(x,y,z),u) = 1     # label("Ka").
a(K(x,y),z,u) = 1     # label("aK1").
a(x,K(y,z),u) = 1     # label("aK2").
a(x,y,K(z,u)) = 1     # label("aK3").

% aa (or "double-a") goals
a(a(x,y,z),u,w) = 1   # label("aa1").
a(x,a(y,z,u),w) = 1   # label("aa2").
a(x,y,a(z,u,w)) = 1   # label("aa3").

end_of_list.
```
Double-a Goals
• The 3 goals are equivalent.

• Proved for several special cases.

• Example next step challenge: middle Bol + KK => aa1.
```   x * ((y * z) \ x) = (x / z) * (y \ x)    # label("middle Bol").
K(K(x,y),z) = 1                          # label("KK").
```

• Another example challenge: AIM => any aai_eq_aaj.

• Results assuming middle Bol as an extra assumption