Agree 100% on wanting machinr verification of AI generated math.

But in regards to beauty, i feel like multiplication already has a lot of non beautiful exponents. Best known matrix multiply is O(n^2.371). For integer factorization, the inverse of this problem, general number field sieve is a crazy subexponential.

If factorization is just barely subexponential, is it really that surprising that multiplication is just barely sub n lg n ?