Comment by criemen
12 hours ago
The thing that I've not fully groked here (might be relevant) is that OAI is generating "paper" proofs first, and only then formalizes them in Lean as a separate step. They've as far as I'm aware not said anywhere how many write ups failed formalization due to a bug in the proof. If we assume that number is low, models would be quite good at one-shotting math proofs. Then it depends if you can replicate the math RL training for chemistry/biology/medicine. Is there enough data out there for that? No idea.
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.).
Wouldn't a bug in the (Lean) kernel just result in a PR to Lean?
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.