OpenAI publishes 719 model-produced math manuscripts, about 42% Lean-formalized