Comment by measurablefunc
1 day ago
Seems kinda odd then that it didn't occur to OpenAI to iterate until they reached a fixedpoint for both the informal & formal development b/c it's obvious that correspondence should have been part of their training pipeline.
Their aim was to create a correct-looking proof using as little resources as possible, not to create a correct proof.