{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:25:53Z","timestamp":1772119553644,"version":"3.50.1"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T00:00:00Z","timestamp":1747612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T00:00:00Z","timestamp":1747612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100012818","name":"Comunidad de Madrid","doi-asserted-by":"publisher","award":["IAxEM-CM\/PHS-2024\/PH-HUM-383"],"award-info":[{"award-number":["IAxEM-CM\/PHS-2024\/PH-HUM-383"]}],"id":[{"id":"10.13039\/100012818","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012818","name":"Comunidad de Madrid","doi-asserted-by":"publisher","award":["IAxEM-CM\/PHS-2024\/PH-HUM-383"],"award-info":[{"award-number":["IAxEM-CM\/PHS-2024\/PH-HUM-383"]}],"id":[{"id":"10.13039\/100012818","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1007\/s10472-025-09983-9","type":"journal-article","created":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T02:07:52Z","timestamp":1747620472000},"page":"1011-1033","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated analysis of the difficulty of secondary school geometry theorems"],"prefix":"10.1007","volume":"93","author":[{"given":"Soma","family":"Bartha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"Kerekes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zolt\u00e1n","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1s","family":"Recio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,19]]},"reference":[{"key":"9983_CR1","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, Z., Recio, T., V\u00e9lez, M.P.: Automated reasoning tools with GeoGebra: What are they? What are they good for? In: Richard, P.R., V\u00e9lez, M.P., Van Vaerenbergh, S. (eds.) Mathematics education in the age of artificial intelligence: how artificial intelligence can serve mathematical human learning, pp. 23\u201344. Springer, (2022). https:\/\/doi.org\/10.1007\/978-3-030-86909-0_2","DOI":"10.1007\/978-3-030-86909-0_2"},{"issue":"2","key":"9983_CR2","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/3493492.3493495","volume":"55","author":"Z Kov\u00e1cs","year":"2021","unstructured":"Kov\u00e1cs, Z., Recio, T., V\u00e9lez, M.P.: Automated reasoning tools in GeoGebra Discovery. ACM Commun. Comput. Algebra 55(2), 39\u201343 (2021). https:\/\/doi.org\/10.1145\/3493492.3493495","journal-title":"ACM Commun. Comput. Algebra"},{"key":"9983_CR3","unstructured":"Kov\u00e1cs, Z., Recio, T., V\u00e9lez, M.P.: GeoGebra Automated Reasoning Tools: why and how (to use them in the classroom). In: The 28nd International Conference on Applications of Computer Algebra ACA\u20192023, Program & Abstracts (2023). https:\/\/iit.sggw.edu.pl\/wp-content\/uploads\/sites\/18\/2023\/07\/ACA2023_Program_Abstracts-1.pdf?x58870"},{"key":"9983_CR4","doi-asserted-by":"publisher","unstructured":"Brown, C.W., Kov\u00e1cs, Z., Vajda, R.: Supporting proving and discovering geometric inequalities in GeoGebra by using Tarski. In: Jani\u010di\u0107, P., Kov\u00e1cs, Z. (eds.) Proceedings of the 13th International Conference on Automated Deduction in Geometry, Hagenberg, Austria\/virtual, September 15-17, 2021. Electronic Proceedings in Theoretical Computer Science, vol. 352, pp. 156\u2013166. Open Publishing Association, (2021). https:\/\/doi.org\/10.4204\/EPTCS.352.18","DOI":"10.4204\/EPTCS.352.18"},{"issue":"10","key":"9983_CR5","doi-asserted-by":"publisher","first-page":"22593","DOI":"10.3934\/math.20231151","volume":"8","author":"Z Kov\u00e1cs","year":"2023","unstructured":"Kov\u00e1cs, Z., Recio, T., Ueno, C., Vajda, R.: The \u201cnever-proved\u2019\u2019 triangle inequality: A geogebra & cas approach. AIMS Mathematics 8(10), 22593\u201322642 (2023). https:\/\/doi.org\/10.3934\/math.20231151","journal-title":"AIMS Mathematics"},{"key":"9983_CR6","doi-asserted-by":"publisher","unstructured":"Botana, F., Recio, T., V\u00e9lez, M.P.: On using geogebra and chatgpt for geometric discovery. Computers 13(8) (2024) https:\/\/doi.org\/10.3390\/computers13080187","DOI":"10.3390\/computers13080187"},{"key":"9983_CR7","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, Z., Recio, T., V\u00e9lez, M.P.: Showing proofs, assessing difficulty with GeoGebra Discovery. In: Quaresma, P., Kov\u00e1cs, Z. (eds.) Proceedings 14th International Conference on Automated Deduction in Geometry, Belgrade, Serbia, 20-22th September 2023. Electronic Proceedings in Theoretical Computer Science, vol. 398, pp. 43\u201352. Open Publishing Association, (2024). https:\/\/doi.org\/10.4204\/EPTCS.398.8","DOI":"10.4204\/EPTCS.398.8"},{"key":"9983_CR8","unstructured":"Kov\u00e1cs, Z., Parisse, B., Recio, T., V\u00e9lez, M.P., Yu, J.H.: ShowProof in GeoGebra Discovery: Automated ranking of elementary geometry theorems. Presentation at ISSAC-49, Raleigh, NC, USA (2024)"},{"key":"9983_CR9","doi-asserted-by":"publisher","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms. Springer (2007). https:\/\/doi.org\/10.1007\/978-0-387-35651-8","DOI":"10.1007\/978-0-387-35651-8"},{"key":"9983_CR10","doi-asserted-by":"publisher","unstructured":"Ari\u00f1o-Morera, B., Kov\u00e1cs, Z., Recio, T., Tolmos, P.: Solving with GeoGebra Discovery an Austrian mathematics olympiad problem: Lessons learned. In: Quaresma, P., Kov\u00e1cs, Z. (eds.) Proceedings 14th international conference on automated deduction in geometry, Belgrade, Serbia, 20-22th September 2023. Electronic Proceedings in Theoretical Computer Science, vol. 398, pp. 101\u2013109. Open Publishing Association, (2024). https:\/\/doi.org\/10.4204\/EPTCS.398.13","DOI":"10.4204\/EPTCS.398.13"},{"key":"9983_CR11","doi-asserted-by":"publisher","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: An introduction to Java Geometry Expert. In: Sturm, T., Zengler, C. (eds.) Automated Deduction in Geometry. ADG 2008. LNCS, vol. 6301. Springer, (2011). https:\/\/doi.org\/10.1007\/978-3-642-21046-4_10","DOI":"10.1007\/978-3-642-21046-4_10"},{"issue":"11","key":"9983_CR12","doi-asserted-by":"publisher","first-page":"1203","DOI":"10.1002\/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N","volume":"30","author":"ER Gansner","year":"2000","unstructured":"Gansner, E.R., North, S.C.: An open graph visualization system and its applications to software engineering. Software-Practice and Experience 30(11), 1203\u20131233 (2000)","journal-title":"Software-Practice and Experience"},{"key":"9983_CR13","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/BF00881868","volume":"10","author":"L Wos","year":"1993","unstructured":"Wos, L.: The problem of automated theorem finding. J. Autom. Reason. 10, 137\u2013138 (1993). https:\/\/doi.org\/10.1007\/BF00881868","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9983_CR14","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1006\/ijhc.2000.0394","volume":"53","author":"S Colton","year":"2000","unstructured":"Colton, S., Bundy, A., Walsh, T.: On the notion of interestingness in automated mathematical discovery. Int. J. Hum. Comput. Stud. 53(3), 351\u2013375 (2000). https:\/\/doi.org\/10.1006\/ijhc.2000.0394","journal-title":"Int. J. Hum. Comput. Stud."},{"key":"9983_CR15","unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: Sutcliffe, G.C.J. (ed.) Proceedings of the nineteenth international florida artificial intelligence research society conference (FLAIRS 2006), pp. 49\u201354 (2006)"},{"key":"9983_CR16","doi-asserted-by":"crossref","unstructured":"Gao, H., Goto, Y., Cheng, J.: Explicitly epistemic contraction by predicate abstraction in automated theorem finding: A case study in nbg set theory. In: Nguyen, N.T. (ed.) Intelligent Information and Database Systems, 7th Asian Conference, ACIIDS 2015, Bali, Indonesia, March 23-25, 2015, Proceedings, Part I, Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), vol. 9011, pp. 593\u2013602. Springer, (2015)","DOI":"10.1007\/978-3-319-15702-3_57"},{"key":"9983_CR17","doi-asserted-by":"publisher","unstructured":"Gao, H., Li, J., Cheng, J.: Measuring interestingness of theorems in automated theorem finding by forward reasoning: A case study in tarski\u2019s geometry. In: 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation (SmartWorld\/SCALCOM\/UIC\/ATC\/CBDCom\/IOP\/SCI), pp. 168\u2013173 (2018). https:\/\/doi.org\/10.1109\/SmartWorld.2018.00064","DOI":"10.1109\/SmartWorld.2018.00064"},{"key":"9983_CR18","doi-asserted-by":"publisher","unstructured":"Quaresma, P., Graziani, P., Nicoletti, S.M.: Considerations on approaches and metrics in automated theorem generation\/finding in geometry. In: Proceedings ADG 2023 (2023). https:\/\/doi.org\/10.4204\/EPTCS.398.12","DOI":"10.4204\/EPTCS.398.12"},{"issue":"2","key":"9983_CR19","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1564\/tme_v26.2.06","volume":"26","author":"V Santos","year":"2019","unstructured":"Santos, V., Baeta, N., Quaresma, P.: Geometrography in dynamic geometry. International Journal for Technology in Mathematics Education 26(2), 89\u201396 (2019). https:\/\/doi.org\/10.1564\/tme_v26.2.06","journal-title":"International Journal for Technology in Mathematics Education"},{"key":"9983_CR20","unstructured":"P\u00e1lfalvi, J.: T\u00e9nyek \u00e9s Eml\u00e9kek Egy K\u00f6z\u00e9piskolai Matematikatan\u00edt\u00e1si K\u00eds\u00e9rletr\u0151l. Typotex, (2022)"},{"key":"9983_CR21","unstructured":"Reiman, I.: Fejezetek Az Elemi Geometri\u00e1b\u00f3l. Typotex, (2009)"},{"key":"9983_CR22","volume-title":"Vektorok, Koordin\u00e1tageometria","author":"F Pog\u00e1ts","year":"1992","unstructured":"Pog\u00e1ts, F.: Vektorok, Koordin\u00e1tageometria. Trigonometria, Tank\u00f6nyvkiad\u00f3 V\u00e1llalat (1992)"},{"key":"9983_CR23","unstructured":"Hajnal, I.: Matematika a Speci\u00e1lis Matematika I. oszt\u00e1lya Sz\u00e1m\u00e1ra. Tank\u00f6nyvkiad\u00f3 V\u00e1llalat, (1987)"},{"key":"9983_CR24","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.jsc.2018.04.007","volume":"90","author":"P Boutry","year":"2019","unstructured":"Boutry, P., Braun, G., Narboux, J.: Formalization of the arithmetization of euclidean plane geometry and applications. Journal of Symbolic Computation 90, 149\u2013168 (2019). https:\/\/doi.org\/10.1016\/j.jsc.2018.04.007","journal-title":"Journal of Symbolic Computation"},{"key":"9983_CR25","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, Z., Parisse, B.: Giac and GeoGebra \u2013 improved Gr\u00f6bner basis computations. In: Gutierrez, J., Schicho, J., Weimann, M. (eds.) Computer Algebra and Polynomials. Lecture Notes in Computer Science, pp. 126\u2013138. Springer, (2015). https:\/\/doi.org\/10.1007\/978-3-319-15081-9_7","DOI":"10.1007\/978-3-319-15081-9_7"},{"key":"9983_CR26","unstructured":"Decker, W., Greuel, G.-M., Pfister, G., Sch\u00f6nemann, H.: Singular 4-4-0 \u2014 A computer algebra system for polynomial computations. https:\/\/www.singular.uni-kl.de (2024)"},{"key":"9983_CR27","doi-asserted-by":"publisher","unstructured":"Thaller, A., Kov\u00e1cs, Z.: Online generation of proofs without words. In: Jani\u010di\u0107, P., Kov\u00e1cs, Z. (eds.) Proceedings of the 13th international conference on automated deduction in geometry, Hagenberg, Austria\/virtual, September 15-17, 2021. Electronic Proceedings in Theoretical Computer Science, vol. 352, pp. 103\u2013105. Open Publishing Association, (2021). https:\/\/doi.org\/10.4204\/EPTCS.352.10","DOI":"10.4204\/EPTCS.352.10"},{"key":"9983_CR28","doi-asserted-by":"publisher","unstructured":"Winkler, F.: Polynomial Algorithms in Computer Algebra. Springer (1996). https:\/\/doi.org\/10.1007\/978-3-7091-6571-3","DOI":"10.1007\/978-3-7091-6571-3"},{"key":"9983_CR29","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: the Calculus of Inductive Constructions. Springer, (2013)"},{"key":"9983_CR30","unstructured":"Pottier, L.: Connecting Gr\u00f6bner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Knowledge Exchange: Automated Provers and Proof Assistants. CEUR Workshop Proceedings, vol. 418. CEUR-WS.org, (2008). http:\/\/hal.inria.fr\/inria-00504727\/en\/"},{"key":"9983_CR31","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Pottier, L., Th\u00e9ry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Post-proceedings of Automated Deduction in Geometry (ADG 2008). Lecture Notes in Artificial Intelligence, vol. 6301, pp. 42\u201359. Springer, (2011)","DOI":"10.1007\/978-3-642-21046-4_3"},{"key":"9983_CR32","doi-asserted-by":"publisher","unstructured":"G\u00e9nevaux, J.-D., Narboux, J., Schreck, P.: Formalization of Wu\u2019s simple method in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) Lecture Notes in Computer Science, vol. 7086, pp. 71\u201386. Springer-Verlag, (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_8. https:\/\/inria.hal.science\/inria-00618745","DOI":"10.1007\/978-3-642-25379-9_8"},{"issue":"2","key":"9983_CR33","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/3712023.3712026","volume":"58","author":"Z Kov\u00e1cs","year":"2024","unstructured":"Kov\u00e1cs, Z., Parisse, B., Recio, T., V\u00e9lez, M.P., Yu, J.H.: The ShowProof command in GeoGebra Discovery: Towards the automated ranking of elementary geometry theorems. ACM Commun. Comput. Algebra 58(2), 27\u201330 (2024). https:\/\/doi.org\/10.1145\/3712023.3712026","journal-title":"ACM Commun. Comput. Algebra"},{"key":"9983_CR34","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, Z., Vujic, A.: Open source prover in the attic. In: Quaresma, P., Kov\u00e1cs, Z. (eds.) Proceedings 14th international conference on automated deduction in geometry, Belgrade, Serbia, 20-22th September 2023. Electronic Proceedings in Theoretical Computer Science, vol. 398, pp. 53\u201361. Open Publishing Association, (2024). https:\/\/doi.org\/10.4204\/EPTCS.398.9","DOI":"10.4204\/EPTCS.398.9"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-025-09983-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-025-09983-9","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-025-09983-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,3]],"date-time":"2026-01-03T07:19:15Z","timestamp":1767424755000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-025-09983-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,19]]},"references-count":34,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9983"],"URL":"https:\/\/doi.org\/10.1007\/s10472-025-09983-9","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-5459295\/v1","asserted-by":"object"}]},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,19]]},"assertion":[{"value":"22 April 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 May 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}