Ever since the landmark PPAD-completeness result for Nash equilibria in two-player normal-form games, significant research has focused on developing polynomial-time algorithms for \(\epsilon \) -approximate Nash equilibria ( \(\epsilon \) -NE). The challenge of establishing the optimal approximation guarantee in polynomial time remains pivotal. While advancements have been made for two-player games, progress in multi-player games is still limited. Difficulties arise due to the increased sophistication of multi-player games and the lack of tools for analyzing approximation bounds. This paper presents a method that allows machines to perform approximation analysis for multi-player games using a domain-specific language called LegoNE. LegoNE enables researchers to design algorithms with only high-level intuitions, while it automatically uncovers the underlying structures and proves the approximation bounds on its own. Using LegoNE, we design a new algorithm for three-player games that achieves a \((0.5+\delta )\) -NE, improving the previous best bound \((0.6+\delta )\) . This shows that human-machine collaboration allows us to obtain higher-level understandings and better results.