Are OpenAI's math results "creative" in an important way?

Many people expect the AI paradigm to approximately AGI complete, and expect it to smoothly scale to AI that can do innovative science. i.e. the kind of science you'd need to do to develop a plague from scratch that actually kills all humans, with very limited opportunity to experiment. Or, the kind of science you'd need to solve alignment, so you could build a more powerful successor AI that shares your values.

A periodic thread of disagreement has been @TsviBT, @Steven Byrnes and some others arguing that, yes, the AIs are getting better at verifiable tasks, but they still seem to be missing some basic sauce that lets them actually form new concepts on the fly and apply them.

The AIs are getting better at "brute force creativity", where you try every single idea ever devised by Man in parallel and maybe one of them works. But there's still a kind of creativity that a) would have way higher efficiency and b) is maybe necessary for doing some kinds of breakthrough work.

On one hand, my subjective experience has been seeing AIs be able to demonstrate increasingly interesting judgement and taste in increasingly many domains (even open-ended ones). But, I do indeed still run into AIs that get confused and "just don't get it", in a way that is pretty suggestive that there is still something significant missing.

OpenAI has lately been shipping some major results in mathematics, for problems that people had previously agreed were important and hard. But, I'd heard for previous results that the proofs turned out sort of "not actually interesting", compared to how sometimes makes you go "Holy shit that's beautiful/elegant/surprising" and conveys someone is a level above you."

Recently they shipped a lot of new proofs on important problems.

I'm not a math guy. But, seems fairly important for some people with enough context to wade through them and figure out "What sort of cognition was involved here?". Do any of the proofs have the vibe of AlphaGo's Move 37? Does it invent a new concept that does real work?

I'm guessing answering this is a nontrivial task that'll involve some... archaeology? Might be cool for a competent math theorist who doesn't have a higher priority project to organize the labor. (I'm guessing the broader math community will do this on their own, but not necessarily organize the information in a way that's optimized for figuring out "is this the kind of mind that could solve its own alignment or quickly develop radically more powerful weapons than we have available?".

I'm shamelessly copying in @DaemonicSigil's quick take about this, to give some hooks for people to start thinking through.

OpenAI releases solutions to many open problems in mathematics. They provide both lean proofs and preprints in a git repo. We knew they were working on this, now it has been released.Some results that I thought were interesting include (numbers from this document):#4: Hilbert's 10th problem was resolved negatively 1970. It asks if there is an algorithm to determine whether a multi-variable polynomial with integer coefficients has an integer root. This is a generalization of that result to rational roots: It shows that no algorithm that can decide whether a polynomial with integer coefficients has a rational root.#5: Catalan's constant is irrational.#17: The irrationality exponent of is 2 (same as most other real numbers).#25: Every rational can be written as an Egyptian fraction of length .#28: The Gaussian moat conjecture is true. Here is what it says: Pretend the Gaussian primes are islands and the rest of is ocean. Suppose we can kayak a distance before we need to stop and rest at an island. Then there is no value of large enough to allow us to make a journey from the origin to infinity.#102: The Unique Games Conjecture is true.#103: L = RL = BPL, i.e. probabilistic algorithms with logarithmic space complexity can be de-randomized to deterministic algorithms with logarithmic space complexity.#107: Matrix multiplication in time.#109: Integer multiplication (slightly) faster than .#130: Fourier transforms (slightly) faster than . As measured by the number of arithmetic operations.#137: One-tape Turing machines that run in time can be simulated in space.#155: There is a tile that forces aperiodic tiling of and under the rule that we're not allowed to rotate the tiles.#158: The chromatic number of (the unit distance graph of) the plane is greater than 5.#241: "Rigidity of Turing Degrees": No non-trivial relabelling of Turing degrees preserves their order.#261: Characterize spectrum of lattice Anderson model in dimension 2 vs 3 or more dimensions.#363: Demonstrate two solutions of the Boltzmann equation for hard spheres, with the same initial conditions.