By combining Wu's method with traditional synthetic methods of deductive databases and angle, ratio, and distance chasing, the authors were able to solve 21 out of 30 problems using only a CPU-only laptop with a time limit of 5 minutes per problem. This approach solved only 4 problems less than AlphaGeometry and is the first fully symbolic baseline strong enough to rival an IMO silver medalist. Furthermore, Wu's method solved 2 problems that AlphaGeometry could not. By combining AlphaGeometry with Wu's method, the authors set a new standard for automated theorem proving on IMO-AG-30, solving 27 out of 30 problems, surpassing the performance of an IMO gold medalist.
Key takeaways:
- The introduction of AlphaGeometry, a neuro-symbolic model, marked a significant advancement in automated theorem proving, solving 25 out of 30 International Mathematical Olympiad (IMO) problems.
- Wu's method, a baseline method, was found to be surprisingly strong, solving 15 problems, some of which were not solved by other methods.
- Combining Wu's method with classic synthetic methods of deductive databases and angle, ratio, and distance chasing solves 21 out of 30 problems, establishing a strong fully symbolic baseline.
- By combining AlphaGeometry with Wu's method, a new state-of-the-art for automated theorem proving on IMO-AG-30 was set, solving 27 out of 30 problems, outperforming an IMO gold medalist for the first time.