For those in academics, is OpenAI the vendor of choice?

A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation.

LLMs are just the beginning, we'll see more specialized math AI resembling StockFish soon.

- It does not show an example of the new best solution, nor explain why they couldn't show an example (e.g. if the proof was not constructive)

- It does not even explain the previous best solution. The diagram of the rescaled unit grid doesn't indicate what the "points" are beyond the normal non-scaled unit grid. I have no idea what to take away from it.

- It's description of the new proof just cites some terms of art with no effort made to actually explain the result.

If this post were not on the OpenAI blog, I would assume it was slop. I understand advanced pure mathematics is complicated, but it is entirely possible to explain complicated topics to non-experts.

Ayer, and in a different way early Wittgenstein, held that mathematical truths don’t report new facts about the world. Proofs unfold what is already implicit in axioms, definitions, symbols, and rules.

I think that idea is deeply fascinating, AND have no problem that we still credit mathematicians with discoveries.

So either “recombining existing material” isn’t disqualifying, or a lot of Fields Medals need to be returned.