The geometry problem was not fully solved, in the sense that AlphaGeometry2 does not prove that the construction is feasible, as far as I understand, they do not construct point X and Y, they assume that such a construction exists " coll x b c; x != c; foot d i b c; perp x t1 t1 i; cong i t1 i d; para x t1 a c;" " We manually construct an approximate diagram. " (https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html#:~:text=Solution%20(reversed%20proof)-,Formalization,-%3A) I was very surprised to see that they claim their solution would get a 7/7 mark. Especially since the construction of points X and Y is not complicated. When they made the announcement of AlphaGeometry version 1, they claimed to solve 25 OIM geometry problems since 2000. In fact, for two of them, they only proved an implication instead of an equivalence.
AlphaGeometry2 is also presented as two orders of magnitude more efficient than AlphaGeometry. Looks like impressive, but it's not that good, it's still about three orders or magnitude less efficient than Giac/Xcas. I have put a page of solutions of 41/42 OIM geometry problems since 2000, they run in the browser in at most a couple of seconds each: https://xcas.univ-grenoble-alpes.fr/forum/viewtopic.php?f=32&t=2891 The solutions are also available in the check directory of the source code of Giac (./chk_oim). On Monday, July 29, 2024 at 9:01:43 AM UTC+2 Kwankyu Lee wrote: > Down to earth, chatgpt on my phone surprised me by solving my final exam > statistics problem just from the photo of the exam sheet in Korean :-) > Problems with a "standard" procedural answer seems a piece of cake to it. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/e9d85101-2c18-4bcc-8727-a84e9ab90838n%40googlegroups.com.
