I'm seeing estimates of a %95-91 failure rate on attempts in generally (or, conversely, a max of ~10% success, but likely lower, since we can only go based on how many attempts they are willing to mention in their statements). E.g., from analysis in https://medium.com/@mehmet.ozel2701/openai-tried-about-4-000...

I wonder how many of those founder at the "paper" to formalization step, or at earlier or later steps (e.g., proof doesn't turn out to prove what the paper said, hits a bug in the kernel, etc.).

based on how bad these models are at one-shotting complex real-world software engineering problems -- it always has to be a conversation -- there is absolutely no way they're one-shotting complex math proofs.

Also, goes without saying, but put Sam Altman in jail, obviously.