{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T23:07:37Z","timestamp":1764198457691,"version":"3.46.0"},"publisher-location":"Singapore","reference-count":32,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819549597"},{"type":"electronic","value":"9789819549603"}],"license":[{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-4960-3_34","type":"book-chapter","created":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T04:58:39Z","timestamp":1764133119000},"page":"421-434","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Planning to\u00a0Prove: Improving Informal Proofs of\u00a0Olympiad Inequalities from\u00a0Large Language Models"],"prefix":"10.1007","author":[{"given":"Le Van","family":"Thanh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Do Xuan","family":"Trong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pham Duc","family":"Tinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hai Van","family":"Pham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,27]]},"reference":[{"key":"34_CR1","unstructured":"Naveed, H., et al.: A comprehensive overview of large language models. ACM Trans. Intell. Syst. Technol. (2023)"},{"key":"34_CR2","doi-asserted-by":"publisher","first-page":"26839","DOI":"10.1109\/ACCESS.2024.3365742","volume":"12","author":"MAK Raisan","year":"2024","unstructured":"Raisan, M.A.K., et al.: A review on large language models: architectures, applications, taxonomies, open issues and challenges. IEEE Access 12, 26839\u201326874 (2024)","journal-title":"IEEE Access"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Pham, H.V., Moore, P.: Applied hedge algebra approach with multilingual large language models to extract hidden rules in datasets for improvement of generative AI applications. Information 15(7) (2024). ISSN 2078-2489","DOI":"10.3390\/info15070381"},{"key":"34_CR4","doi-asserted-by":"publisher","first-page":"57","DOI":"10.3390\/informatics11030057","volume":"11","author":"ZA Nazi","year":"2024","unstructured":"Nazi, Z.A., Peng, W.: Large language models in healthcare and medical domain: a review. Informatics 11, 57 (2024)","journal-title":"Informatics"},{"issue":"10","key":"34_CR5","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pone.0292216","volume":"18","author":"M Hosseini","year":"2023","unstructured":"Hosseini, M., et al.: An exploratory survey about using chatGPT in education, healthcare, and research. PLoS ONE 18(10), e0292216 (2023)","journal-title":"PLoS ONE"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Siino, M., Falco, M., Croce, D., Rosso, P.: Exploring LLMs applications in law: a literature review on current legal NLP approaches. IEEE Access (2025)","DOI":"10.1109\/ACCESS.2025.3533217"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Huang, X., Shen, Q., Hu, Y., Gao, A., Wang, B.: LLMs for mathematical modeling: towards bridging the gap between natural and mathematical languages. In: Findings of the Association for Computational Linguistics: NAACL 2025, pp. 2678\u20132710. Association for Computational Linguistics (2025). ISBN 979-8-89176-195-7","DOI":"10.18653\/v1\/2025.findings-naacl.146"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"Tuan, N.T., Moore, P., Thanh, D.H.V., Pham, H.V.: A generative artificial intelligence using multilingual large language models for chatGPT applications. Appl. Sci. 14(7) (2024). ISSN 2076-3417","DOI":"10.3390\/app14073036"},{"key":"34_CR9","first-page":"19783","volume":"37","author":"A Didolkar","year":"2024","unstructured":"Didolkar, A., et al.: Metacognitive capabilities of LLMs: an exploration in mathematical problem solving. Adv. Neural. Inf. Process. Syst. 37, 19783\u201319812 (2024)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"Khan, W.A., Arooj, Y., Pham, H.V.: Modeling academic social networks using covering and matching in intuitionistic fuzzy influence graphs. Symmetry 17(5) (2025)","DOI":"10.3390\/sym17050785"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Khan, W.A., Ahmed Shah, I., Tuan Nguyen, T., Hoan Pham, M., Van Pham, H.: Some concepts of interval valued Pythagorean fuzzy graphs and analysis of socioeconomic conditions of communities. IEEE Access 13, 55\u00a0140\u201355\u00a0155 (2025)","DOI":"10.1109\/ACCESS.2025.3553351"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Khan, W.A., Bushra, M., Tuan Nguyen, T., Hoan Pham, M., Van Pham, H.: Some novel concepts of bipolar picture fuzzy influence graphs models with application toward MADM. IEEE Access 13, 15\u00a0773\u201315\u00a0794 (2025)","DOI":"10.1109\/ACCESS.2025.3530009"},{"key":"34_CR13","unstructured":"Li, Z., et al.: A survey on deep learning for theorem proving. In: First Conference on Language Modeling (2024)"},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"Xia, S., Li, X., Liu, Y., Wu, T., Liu, P.: Evaluating mathematical reasoning beyond accuracy. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 39, pp. 27\u00a0723\u201327\u00a0730 (2025)","DOI":"10.1609\/aaai.v39i26.34987"},{"key":"34_CR15","unstructured":"DeepSeek-AI, et al.: DeepSeek-RL: incentivizing reasoning capability in LLMs via reinforcement learning, CoRR, vol. abs\/2501.12948 (2025)"},{"key":"34_CR16","unstructured":"Jaeh, A., et al.: OpenAI OL system card, arXiv preprint arXiv:2412.16720 (2024)"},{"key":"34_CR17","unstructured":"Cobb, K., et al.: Training verifiers to solve math word problems, CoRR, vol. abs\/2110.14168 (2021). arXiv:2110.14168"},{"key":"34_CR18","unstructured":"Hendrycks, D., et al.: Measuring mathematical problem solving with the MATH dataset. In: Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2) (2021)"},{"issue":"9","key":"34_CR19","first-page":"9","volume":"13","author":"J Li","year":"2024","unstructured":"Li, J., et al.: Numinamath: the largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face Repository 13(9), 9 (2024)","journal-title":"Hugging Face Repository"},{"key":"34_CR20","unstructured":"Luo, H., et al.: WizardMath: empowering mathematical reasoning for large language models via reinforced evol-instruct. In: The Thirteenth International Conference on Learning Representations (2024)"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"Zhang, D., et al.: LLaMA-berry: pairwise optimization for olympiad-level mathematical reasoning via OL-like Monte Carlo tree search. In: Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), pp. 7315\u20137337. Association for Computational Linguistics (2025)","DOI":"10.18653\/v1\/2025.naacl-long.375"},{"key":"34_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"34_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-35746-6_3","volume-title":"Tools for Practical Software Verification","author":"C Paulin-Mohring","year":"2012","unstructured":"Paulin-Mohring, C.: Introduction to the Coq proof-assistant for practical software verification. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 45\u201395. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_3"},{"key":"34_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant For Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant For Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"34_CR25","unstructured":"Yang, K., et al.: LeanDojo: theorem proving with retrieval-augmented language models. In: Thirty-seventh Conference on Neural Information Processing Systems Datasets and Benchmarks Track (2023)"},{"key":"34_CR26","unstructured":"Xin, H., et al.: Advancing theorem proving in LLMs through large-scale synthetic data. In: The 4th Workshop on Mathematical Reasoning and AI at NeurIPS 2024 (2024)"},{"key":"34_CR27","unstructured":"Welleck, S., Liu, J., Bras, R.L., Hajishirizi, H., Choi, Y., Cho, K.: NaturalProofs: mathematical theorem proving in natural language. In: Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1) (2021)"},{"key":"34_CR28","first-page":"4913","volume":"35","author":"S Welleck","year":"2022","unstructured":"Welleck, S., Liu, J., Lu, X., Hajishirizi, H., Choi, Y.: NaturalProver: grounded mathematical proof generation with language models. Adv. Neural. Inf. Process. Syst. 35, 4913\u20134927 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"34_CR29","unstructured":"Wei, C., Sun, M., Wang, W.: Proving Olympiad algebraic inequalities without human demonstrations. In: The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track (2024)"},{"key":"34_CR30","unstructured":"Li, Z., et al.: Proving Olympiad inequalities by synergizing LLMs and symbolic reasoning. In: The Thirteenth International Conference on Learning Representations (2025)"},{"key":"34_CR31","unstructured":"Sheng, J., et al.: Solving inequality proofs with large language models, arXiv preprint arXiv:2506.07927 (2025)"},{"key":"34_CR32","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"}],"container-title":["Lecture Notes in Computer Science","Multi-disciplinary Trends in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4960-3_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T23:03:06Z","timestamp":1764198186000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4960-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,27]]},"ISBN":["9789819549597","9789819549603"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4960-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,27]]},"assertion":[{"value":"27 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MIWAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Multi-disciplinary Trends in Artificial Intelligence","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ho Chi Minh City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vietnam","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":"3 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"miwai2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/miwai25.miwai.org","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}