What does a superhuman level of mathematics look like? Here is one elementary example I could give to nonexperts. Daniel Kane and Terence Tao showed (arxiv.org/abs/1702.00912) that, given a collection X of sets, the total number of ways to write A as a disjoint union of B and C, with A, B, C from X (disjoint means non-overlapping), is at most cardinality of X to the power 1.72598…, and this power is sharp. To show this, they came up with an innocent-looking function B(x,y,z) = (xyz)^c of three variables, satisfying a certain arithmetic inequality and having prescribed boundary conditions. Proving that arithmetic inequality was really a headache. There was a question whether one could improve this bound, i.e., maybe add some logarithmic correction terms, and one could kind of imagine what should be done (see comments on terrytao.wordpress.com/2017/…), but it was not clear whether it would be easy to do. Now superintelligence improves this bound by introducing a certain monster function of three variables (see screenshot). Even if I had seen this function in my dreams, I would never have dared to verify that main arithmetic inequality. The candidate function produced by SI gives a bound matching the known lower-bound examples up to a constant factor, including the sharp logarithmic correction. All the details are here paatai.github.io/ai-proofs/b…

We've updated our GitHub math repo with 6 new Lean formalizations, 19 modifications, and 3 withdrawals. The repo now has ~42% top-line results formalized. We will continue to update the repo with new formalizations and with any errata we notice. github.com/openai/math/blob/…