Did they remember what OpenAI did with Lean and Math Proofs?

OpenAI wrote some lean that pass the validate, write a math paper that feel plausible, but the paper don't match what's in lean.

Anthropic is now translating programs into Rocq proof. The same can happen.

Don't get me wrong -- this process can help catch some bug. but this is far from a proof