It's even conceivable that 2 gets worse with AI: The AI does the proof for them, very convolutedly so, and as long as the proof checker eats it, it goes through. Comes the day when the complexity goes beyond what the AI assistant can handle and it gives up. At that point, the proof codes complexity will for a long time have passed the threshold of being comprehensible for any human and there is no progress possible. Hard stop.