Comment by bamb008

In [1] they claim:

>However, there were 34 noteworthy deviations from the published record that needed to be resolved, the most substantial of which related to the Unbalanced Group Theorem.

[1]https://axiommath.ai/research/the-enormous-theorem-formalize...