The recent drop from OpenAI with 372 result families and 719 papers is impressive in the kind of conjectures it potentially proves. Note that mistakes in the proofs are very much possible, especially in the papers with no Lean certificate, so this should be mostly viewed as raw material to work with rather than any sort of finished results. Arguably the single most impressive result is the proof of quasi-Riemann hypothesis: \zeta does not have roots with \Re(z)>7/8. I am sure it will be improved in the coming weeks (it has already been improved by a tiny bit here) but accroding to those who've read the proof, this approach would not get us beyond 3/4, so this is still very far from actually proving RH. Among other (potentially correct) results is the proof of conformal invariance of FK model on the plane, computation of critical exponent for displacement for the self-avodiing walk on the hexagonal lattice, Polyakov's conjecture, critical exponents for the BKT transition of XY model, and many other results in statistical mechanics. A lot to work with! I am particularly interested in understanding the ideas which went into the proof for the self-avoiding walk, would be exciting to understand what is going on. There are also many results in additive combinatorics, including the famous conjecture of Erdos: if a set A of positive integers has sum of reciprocals of its elements diverging then A contains arbitrary long arithmetic progressions. In fact, they prove a much sharper result for the density of set A but only this weaker conjecture seems to have been formalised whereas the whole paper is 198 pages (still much shorter than the proof for the self-avoiding walk which is 13 papers spanning 1060 pages or so). One other result, which is related to my paper above, is that OpenAI indeed proves that square-difference-free subset of {1, 2, ..., N} has size at most N^{1-c} where c>0 is an absolute constant. Anyhow, I hope to see a lot of progress related to these results in human mathematics. I don't think people should be trying to understand these proofs per se but instead use them as a source of ideas to work with. Also note that these capabilities will likely soon be publicly available so mathematicians should quickly adapt to the reality in which getting formally verified proofs of previously impressive conjectures is relatively cheap.