4 ms·
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 formal
by shmoil 25d ago
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 25d agoWas the proof correct?
- voxl 25d agoNo 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.
- 9864325789976 24d agoYou forgot to include empirical evidence of your claim, since I'd like to double check it.
- shmoil 23d agoNah, I tried to post a long reply yesterday, but YC was glitching, so I just gave up.