OpenAI's 722 machine-generated maths papers: the hard part is now checking them
An unreleased internal model produced 722 manuscripts, including claimed progress on the unique games conjecture. Only part of the main results come with Lean formalizations, and the field is split on what that is worth.
Read the full summary