AI Helped Me Tackle One of Math's Greatest Mysteries

Post by nujsii » Tue, Aug 20, 2024, 8:17 AM UTC

Circled wrote: post #7

DoctorOetker wrote: post #6

Earlier quoted context omitted.

Are you the author of this paper? the mismatching LHS and RHS would be detected by 12y olds. Perhaps you are this young, in which case I approve of your attempts. Otherwise you are piping AI nonsense to the crowd which I disapprove of. So I assume you mean "Alternative formulation of the proof" in section 6: This relies on Lemma 15, which is right after where I gave up after about 3 basic errors. So let me continue.…

thanks for the input. indeed very kind of you to take the time. I guess it cannot be fixed then? actually the whole idea is to solve it with AI solely as an experiment. and of course human feedback is allowed. so since that was outlined clearly i am not piping nonsense to the crowd. like a turing test maybe...congrats, you passed ;) but i did take it offline since there is no value...

Post by thomas112 » Wed, Aug 21, 2024, 11:13 AM UTC

DoctorOetker wrote: post #8

Circled wrote: post #7

Earlier quoted context omitted.

thanks for the input. indeed very kind of you to take the time. I guess it cannot be fixed then? actually the whole idea is to solve it with AI solely as an experiment. and of course human feedback is allowed. so since that was outlined clearly i am not piping nonsense to the crowd. like a turing test maybe...congrats, you passed ;) but i did take it offline since there is no value...

Oh, I certainly believe deep learning can solve mathematical problems at rates much higher than humans. But that would require using formal verifiers like metamath in the training loop. https://us.metamath.org/ BTW if you found the experience slightly embarassing, get acquainted with metamath, and its interactive prover "mmj2", and the "set.mm" database. everything you prove in mmj2 is guaranteed to be correct (as lo…