{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:35:14Z","timestamp":1757619314033,"version":"3.44.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986840"},{"type":"electronic","value":"9783031986857"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We introduce , a unified and versatile Python-based formal system for representing and reasoning about plane geometry problems.  designs a new formal language that faithfully encodes geometric information, including diagrams, and integrates two complementary components to perform geometric reasoning: (1) a deductive database with an extensive set of inference rules for geometric properties, and (2) an algebraic system for solving diverse equations involving geometric quantities. By seamlessly combining these components,  enables human-like reasoning and supports generating concise reasoning steps (proofs), either fully automatically or through interactive guidance. Benchmark evaluations demonstrate that  outperforms existing tools, solving a broader range of problems across both proof generation and calculation tasks. Moreover,  holds significant potential for educational use and integration with advanced deep learning systems.\n<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_20","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:33:04Z","timestamp":1753155184000},"page":"405-420","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["PyEuclid: A Versatile Formal Plane Geometry System in\u00a0Python"],"prefix":"10.1007","author":[{"given":"Zhaoyu","family":"Li","sequence":"first","affiliation":[]},{"given":"Hangrui","family":"Bi","sequence":"additional","affiliation":[]},{"given":"Jialiang","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Zenan","family":"Li","sequence":"additional","affiliation":[]},{"given":"Kaiyu","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Xujie","family":"Si","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"issue":"4","key":"20_CR1","doi-asserted-by":"publisher","first-page":"700","DOI":"10.1017\/S1755020309990098","volume":"2","author":"J Avigad","year":"2009","unstructured":"Avigad, J., Dean, E., Mumma, J.: A formal system for euclid\u2019s elements. Rev. Symbolic Logic 2(4), 700\u2013768 (2009)","journal-title":"Rev. Symbolic Logic"},{"issue":"1","key":"20_CR2","first-page":"53","volume":"4","author":"MZ Aydogdu","year":"2014","unstructured":"Aydogdu, M.Z., Kesan, C.: A research on geometry problem solving strategies used by elementary mathematics teacher candidates. Online Submission 4(1), 53\u201362 (2014)","journal-title":"Online Submission"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10817-015-9326-4","volume":"55","author":"F Botana","year":"2015","unstructured":"Botana, F., et al.: Automated theorem proving in geogebra: current achievements. J. Autom. Reason. 55, 39\u201359 (2015)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"20_CR4","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1146\/annurev.cs.03.060188.000505","volume":"3","author":"B Buchberger","year":"1988","unstructured":"Buchberger, B., Collins, G.E., Kutzler, B.: Algebraic methods for geometric reasoning. Annual Rev. Comput. Sci. 3(1), 85\u2013119 (1988)","journal-title":"Annual Rev. Comput. Sci."},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Chen, J., et al.: Unigeo: unifying geometry logical reasoning via reformulating mathematical expression. arXiv preprint arXiv:2212.02746 (2022)","DOI":"10.18653\/v1\/2022.emnlp-main.218"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Chen, J., et al.: Geoqa: a geometric question answering benchmark towards multimodal numerical reasoning. arXiv preprint arXiv:2105.14517 (2021)","DOI":"10.18653\/v1\/2021.findings-acl.46"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated production of traditional proofs for constructive geometry theorems. In: [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 48\u201356. IEEE (1993)","DOI":"10.1109\/LICS.1993.287601"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Chou, S.C.: Mechanical geometry theorem proving. Springer (1988)","DOI":"10.1007\/978-94-009-4037-6"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1016\/B978-044450813-3\/50013-8","volume":"1","author":"SC Chou","year":"2001","unstructured":"Chou, S.C., Gao, X.S.: Automated reasoning in geometry. Handbook Autom. Reasoning 1, 707\u2013749 (2001)","journal-title":"Handbook Autom. Reasoning"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants: I. multiple and shortest proof generation. J. Autom. Reasoning 17(3), 325\u2013347 (1996)","DOI":"10.1007\/BF00283133"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants: Ii. theorem proving with full-angles. J. Autom. Reasoning 17(3), 349\u2013370 (1996)","DOI":"10.1007\/BF00283134"},{"issue":"3","key":"20_CR12","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"SC Chou","year":"2000","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reason. 25(3), 219\u2013246 (2000)","journal-title":"J. Autom. Reason."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X., Zhang, J.Z.: Machine proofs in geometry: automated production of readable proofs for geometry theorems, vol.\u00a06. World Scientific (1994)","DOI":"10.1142\/9789812798152"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H Coelho","year":"1986","unstructured":"Coelho, H., Pereira, L.M.: Automated reasoning in geometry theorem proving with prolog. J. Autom. Reason. 2, 329\u2013390 (1986)","journal-title":"J. Autom. Reason."},{"key":"20_CR15","unstructured":"Davis, M.: A computer program for Presburger\u2019s algorithm. Symbolic Comput. Automat. Reason. 1 (1957)"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (1960)","DOI":"10.1145\/321033.321034"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"20_CR18","unstructured":"Gao, J., et\u00a0al.: G-llava: solving geometric problem with multi-modal large language model. arXiv preprint arXiv:2312.11370 (2023)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry theorem machine. In: Papers presented at the May 3-5, 1960, western joint IRE-AIEE-ACM Computer Conference, pp. 143\u2013149 (1960)","DOI":"10.1145\/1460361.1460381"},{"key":"20_CR20","unstructured":"Gelernter, H.L.: Realization of a geometry theorem proving machine. In: International Conference on Information Processing (1959)"},{"key":"20_CR21","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024). https:\/\/www.gurobi.com"},{"issue":"1","key":"20_CR22","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1207\/s1532690xci2401_2","volume":"24","author":"P Herbst","year":"2006","unstructured":"Herbst, P., Brach, C.: Proving and doing proofs in high school geometry classes: what is it that is going on for students? Cogn. Instr. 24(1), 73\u2013122 (2006)","journal-title":"Cogn. Instr."},{"issue":"03","key":"20_CR23","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1109\/MCSE.2007.55","volume":"9","author":"JD Hunter","year":"2007","unstructured":"Hunter, J.D.: Matplotlib: a 2d graphics environment. Comput. Sci. Eng. 9(03), 90\u201395 (2007)","journal-title":"Comput. Sci. Eng."},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/11832225_6","volume-title":"Mathematical Software - ICMS 2006","author":"P Jani\u010di\u0107","year":"2006","unstructured":"Jani\u010di\u0107, P.: GCLC \u2014 a tool for constructive euclidean geometry and more than that. In: Iglesias, A., Takayama, N. (eds.) ICMS 2006. LNCS, vol. 4151, pp. 58\u201373. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11832225_6"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using hilbert\u2019s nullstellensatz. In: Proceedings of the Fifth ACM Symposium on Symbolic and Algebraic Computation, pp. 202\u2013208 (1986)","DOI":"10.1145\/32439.32479"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Automated geometric reasoning: dixon resultants, gr\u00f6bner bases, and characteristic sets. In: Automated Deduction in Geometry: International Workshop on Automated Deduction in Geometry Toulouse, France, 27\u201329 September 1996 Selected Papers 1, pp. 1\u201336. Springer (1997)","DOI":"10.1007\/BFb0022716"},{"key":"20_CR27","unstructured":"Kazemi, M., Alvari, H., Anand, A., Wu, J., Chen, X., Soricut, R.: Geomverse: a systematic evaluation of large models for geometric reasoning. arXiv preprint arXiv:2312.12241 (2023)"},{"issue":"4","key":"20_CR28","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1207\/s15516709cog1404_2","volume":"14","author":"KR Koedinger","year":"1990","unstructured":"Koedinger, K.R., Anderson, J.R.: Abstract planning and perceptual chunks: elements of expertise in geometry. Cogn. Sci. 14(4), 511\u2013550 (1990)","journal-title":"Cogn. Sci."},{"issue":"4","key":"20_CR29","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1016\/S0747-7171(86)80006-2","volume":"2","author":"B Kutzler","year":"1986","unstructured":"Kutzler, B., Stifter, S.: On the application of buchberger\u2019s algorithm to automated geometry theorem proving. J. Symb. Comput. 2(4), 389\u2013397 (1986)","journal-title":"J. Symb. Comput."},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Lu, P., et al.: Inter-gps: interpretable geometry problem solving with formal language and symbolic reasoning. arXiv preprint arXiv:2105.04165 (2021)","DOI":"10.18653\/v1\/2021.acl-long.528"},{"key":"20_CR31","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103","volume":"3","author":"A Meurer","year":"2017","unstructured":"Meurer, A., et al.: Sympy: symbolic computing in python. PeerJ Comput. Sci. 3, e103 (2017)","journal-title":"PeerJ Comput. Sci."},{"key":"20_CR32","unstructured":"Murphy, L., Yang, K., Sun, J., Li, Z., Anandkumar, A., Si, X.: Autoformalizing euclidean geometry. arXiv preprint arXiv:2405.17216 (2024)"},{"issue":"1","key":"20_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"AJ Nevins","year":"1975","unstructured":"Nevins, A.J.: Plane geometry theorem proving using forward chaining. Artif. Intell. 6(1), 1\u201323 (1975)","journal-title":"Artif. Intell."},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Reiter: A semantically guided deductive system for automatic theorem proving. IEEE Trans. Comput. 100(4), 328\u2013334 (1976)","DOI":"10.1109\/TC.1976.1674613"},{"issue":"7995","key":"20_CR35","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1038\/s41586-023-06747-5","volume":"625","author":"TH Trinh","year":"2024","unstructured":"Trinh, T.H., Wu, Y., Le, Q.V., He, H., Luong, T.: Solving olympiad geometry without human demonstrations. Nature 625(7995), 476\u2013482 (2024)","journal-title":"Nature"},{"key":"20_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-61732-9_60","volume-title":"Artificial Intelligence and Symbolic Mathematical Computation","author":"D Wang","year":"1996","unstructured":"Wang, D.: Geometry machines: From AI to SMC. In: Calmet, J., Campbell, J.A., Pfalzgraf, J. (eds.) AISMC 1996. LNCS, vol. 1138, pp. 213\u2013239. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61732-9_60"},{"key":"20_CR37","unstructured":"Waswani, A., et al.: Attention is all you need. In: NIPS (2017)"},{"key":"20_CR38","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BF02328447","volume":"2","author":"W Wen-Tsun","year":"1986","unstructured":"Wen-Tsun, W.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2, 221\u2013252 (1986)","journal-title":"J. Autom. Reason."},{"key":"20_CR39","first-page":"32353","volume":"35","author":"Y Wu","year":"2022","unstructured":"Wu, Y., et al.: Autoformalization with large language models. Adv. Neural. Inf. Process. Syst. 35, 32353\u201332368 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"20_CR40","unstructured":"Xia, R., et\u00a0al.: Geox: Geometric problem solving through unified formalized vision-language pre-training. arXiv preprint arXiv:2412.11863 (2024)"},{"key":"20_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-21046-4_10","volume-title":"Automated Deduction in Geometry","author":"Z Ye","year":"2011","unstructured":"Ye, Z., Chou, S.-C., Gao, X.-S.: An introduction to java geometry expert. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol. 6301, pp. 189\u2013195. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21046-4_10"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T17:20:12Z","timestamp":1757265612000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}