I asked AI to formalize an old important paper in analysis. In the paper there is a sequence of epsilon_n > 0, epsilon_n -> 0. It came back, and said: "I formalized it, it is all good, but the assumption that epsilons > 0 is not used anywhere. Shall we remove it, you a get a stronger result this way?"

LOL

▲

mitxela 5 hours ago | parent [-]

Was the proof correct?

	▲	voxl 17 minutes ago \| parent [-]
		No you see people that use AI generally don't bother to consider this unimportant detail. Or they ask the AI to "double check" its work.