Yes, exactly. There's no real pressure on AI to get the natural language version of the proof correct, and no way to really judge it automatically.