> The idea of puzzling out what an AI did to prove something sounds quite boring and unappealing.

The way I see it, it's no different from a lot of grad student work where you have to figure out what a human-written proof is doing.

> Maybe they could have gotten into contact with the people of the research areas of the problems that they solved and worked with them to create a better exposition.

That's what Anthropic is doing, and the issue is that people will complain that they weren't the chosen "person to work with". OpenAI's approach is more like a race where everyone's at the same starting point: they get the AI's raw proof to work on and have to figure out how it works.