{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T09:44:43Z","timestamp":1777110283969,"version":"3.51.4"},"reference-count":133,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2026,1]]},"DOI":"10.1007\/s11390-026-6040-0","type":"journal-article","created":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:19:50Z","timestamp":1771024790000},"page":"46-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Conjecturing and Theorem Finding: A Survey"],"prefix":"10.1007","volume":"41","author":[{"given":"Jian","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Si-Cheng","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,2,14]]},"reference":[{"issue":"1","key":"6040_CR1","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. Journal of Automated Reasoning, 1993, 10(1): 137\u2013138. DOI: https:\/\/doi.org\/10.1007\/BF00881868.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"6040_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1147\/rd.41.0002","volume":"4","author":"H Wang","year":"1960","unstructured":"Wang H. Toward mechanical mathematics. IBM Journal of Research and Development, 1960, 4(1): 2\u201322. DOI: https:\/\/doi.org\/10.1147\/rd.41.0002.","journal-title":"IBM Journal of Research and Development"},{"key":"6040_CR3","doi-asserted-by":"publisher","DOI":"10.1142\/4132","volume-title":"A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning","author":"L Wos","year":"1999","unstructured":"Wos L, Pieper G W. A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific, 1999. DOI: https:\/\/doi.org\/10.1142\/4132."},{"key":"6040_CR4","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/3-540-52885-7_131","volume-title":"Lecture Notes in Computer Science 449","author":"W McCune","year":"1990","unstructured":"McCune W. Otter 2.0. In Lecture Notes in Computer Science 449, Stickel M E (ed.), Springer, 1990, pp.663\u2013664. DOI: https:\/\/doi.org\/10.1007\/3-540-52885-7_131."},{"key":"6040_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Lecture Notes in Computer Science 8044","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs L, Voronkov A. First-order theorem proving and Vampire. In Lecture Notes in Computer Science 8044, Sharygina N, Veith H (eds.), Springer, 2013, pp.1\u201335. DOI: https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1."},{"issue":"2\/3","key":"6040_CR6","doi-asserted-by":"publisher","first-page":"111","DOI":"10.5555\/1218615.1218621","volume":"55","author":"S Schulz","year":"2002","unstructured":"Schulz S. E - a Brainiac theorem prover. AI Communications, 2002, 55(2\/3): 111\u2013266. DOI: https:\/\/doi.org\/10.5555\/1218615.1218621.","journal-title":"AI Communications"},{"key":"6040_CR7","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Lecture Notes in Computer Science 4963","author":"L de Moura","year":"2008","unstructured":"de Moura L, Bj\u00f8rner N. Z3: An efficient SMT solver. In Lecture Notes in Computer Science 4963, Ramakrishnan C R, Rehof J (eds.), Springer, 2008, pp.337\u2013340. DOI: https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24."},{"key":"6040_CR8","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Lecture Notes in Computer Science 13243","author":"H Barbosa","year":"2022","unstructured":"Barbosa H, Barrett C, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, N\u00f6tzli A, Ozdemir A, Preiner M, Reynolds A, Sheng Y, Tinelli C, Zohar Y. cvc5: A versatile and industrial-strength SMT solver. In Lecture Notes in Computer Science 13243, Fisman D, Rosu G (eds.), Springer, 2022, pp.415\u2013442. DOI: https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24."},{"key":"6040_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L C Paulson","year":"1994","unstructured":"Paulson L C. Isabelle: A Generic Theorem Prover. Springer, 1994. DOI: https:\/\/doi.org\/10.1007\/BFb0030541."},{"key":"6040_CR10","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, 2002. DOI: https:\/\/doi.org\/10.1007\/3-540-45949-9."},{"key":"6040_CR11","series-title":"Technical Report RT-0203","volume-title":"The Coq proof assistant reference manual: Version 6.1","author":"B Barras","year":"1997","unstructured":"Barras B, Boutin S, Cornes C, Courant J, Filli\u00e2tre J C, Gim\u00e9nez E, Herbelin H, Huet G, Mu\u00f1oz C, Murthy C, Parent C, Paulin-Mohring C, Sa\u00efbi A, Werner B. The Coq proof assistant reference manual: Version 6.1. Technical Report RT-0203, INRIA, 1997. https:\/\/inria.hal.science\/inria-00069968, Jan. 2026."},{"key":"6040_CR12","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Lecture Notes in Computer Science 12699","author":"L de Moura","year":"2021","unstructured":"de Moura L, Ullrich S. The Lean 4 theorem prover and programming language. In Lecture Notes in Computer Science 12699, Platzer A, Sutcliffe G (eds.), Springer, 2021, pp.625\u2013635. DOI: https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37."},{"key":"6040_CR13","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Lecture Notes in Computer Science 1166","author":"J Harrison","year":"1996","unstructured":"Harrison J. HOL light: A tutorial introduction. In Lecture Notes in Computer Science 1166, Srivas M, Camilleri A (eds.), Springer, 1996, pp.265\u2013269. DOI: https:\/\/doi.org\/10.1007\/BFb0031814."},{"key":"6040_CR14","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Lecture Notes in Computer Science 1166","author":"B Brock","year":"1996","unstructured":"Brock B, Kaufmann M, Moore J S. ACL2 theorems about commercial microprocessors. In Lecture Notes in Computer Science 1166, Srivas M, Camilleri A (eds.), Springer, 1996, pp.275\u2013293. DOI: https:\/\/doi.org\/10.1007\/BFb0031816."},{"key":"6040_CR15","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-03359-9_5","volume-title":"Lecture Notes in Computer Science 5674","author":"A Naumowicz","year":"2009","unstructured":"Naumowicz A, Korni\u0142owicz A. A brief overview of MIZAR. In Lecture Notes in Computer Science 5674, Berghofer S, Nipkow T, Urban C, Wenzel M (eds.), Springer, 2009, pp.67\u201372. DOI: https:\/\/doi.org\/10.1007\/978-3-642-03359-9_5."},{"key":"6040_CR16","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proc. the 22nd Symposium on Operating Systems Principles","author":"G Klein","year":"2009","unstructured":"Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: Formal verification of an OS kernel. In Proc. the 22nd Symposium on Operating Systems Principles, Oct. 2009, pp.207\u2013220. DOI: https:\/\/doi.org\/10.1145\/1629575.1629596."},{"issue":"7","key":"6040_CR17","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107\u2013115. DOI: https:\/\/doi.org\/10.1145\/1538788.1538814.","journal-title":"Communications of the ACM"},{"key":"6040_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Lecture Notes in Computer Science 5081","author":"G Gonthier","year":"2007","unstructured":"Gonthier G. The four colour theorem: Engineering of a formal proof. In Lecture Notes in Computer Science 5081, Kapur D (ed.), Springer, 2007, Article No. 333. DOI: https:\/\/doi.org\/10.1007\/978-3-540-87827-8_28."},{"issue":"11","key":"6040_CR19","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier G. Formal proof\u2014The four-color theorem. Notices of the American Mathematical Society, 2008, 55(11): 1382\u20131393.","journal-title":"Notices of the American Mathematical Society"},{"key":"6040_CR20","doi-asserted-by":"publisher","first-page":"e2","DOI":"10.1017\/fmp.2017.1","volume":"5","author":"T Hales","year":"2017","unstructured":"Hales T, Adams M, Bauer G, Dang T D, Harrison J, Hoang L T, Kaliszyk C, Magron V, Mclaughlin S, Nguyen T, Nguyen Q T, Nipkow T, Obua S, Pleso J, Rute J, Solovyev A, Ta T H A, Tran N T, Trieu T D, Urban J, Vu K, Zumkeller R. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 2017, 5:e2. DOI: https:\/\/doi.org\/10.1017\/fmp.2017.1.","journal-title":"Forum of Mathematics, Pi"},{"key":"6040_CR21","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1145\/3372885.3373824","volume-title":"Proc. the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs","author":"The Mathlib Community","year":"2020","unstructured":"The Mathlib Community. The Lean mathematical library. In Proc. the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan. 2020, pp.367\u2013381. DOI: https:\/\/doi.org\/10.1145\/3372885.3373824."},{"issue":"1","key":"6040_CR22","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"J C Blanchette","year":"2013","unstructured":"Blanchette J C, B\u00f6hme S, Paulson L C. Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning, 2013, 51(1): 109\u2013128. DOI: https:\/\/doi.org\/10.1007\/s10817-013-9278-5.","journal-title":"Journal of Automated Reasoning"},{"key":"6040_CR23","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/3-540-61511-3_112","volume-title":"Lecture Notes in Computer Science 1104","author":"D Kapur","year":"1996","unstructured":"Kapur D, Subramaniam M. Lemma discovery in automating induction. In Lecture Notes in Computer Science 1104, McRobbie M A, Slaney J K (eds.), Springer, 1996, pp.538\u2013552. DOI: https:\/\/doi.org\/10.1007\/3-540-61511-3_112."},{"key":"6040_CR24","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-23250-4_9","volume-title":"Lecture Notes in Computer Science 11617","author":"M Johansson","year":"2019","unstructured":"Johansson M. Lemma discovery for induction: A survey. In Lecture Notes in Computer Science 11617, Kaliszyk C, Brady E, Kohlhase A, Coen C S (eds.), Springer, 2019, pp.125\u2013139. DOI: https:\/\/doi.org\/10.1007\/978-3-030-23250-4_9."},{"issue":"1","key":"6040_CR25","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A Ireland","year":"1996","unstructured":"Ireland A, Bundy A. Productive use of failure in inductive proof. Journal of Automated Reasoning, 1996, 16(1): 79\u2013111. DOI: https:\/\/doi.org\/10.1007\/BF00244460.","journal-title":"Journal of Automated Reasoning"},{"key":"6040_CR26","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-17172-7_6","volume-title":"Lecture Notes in Computer Science 6463","author":"M Johansson","year":"2010","unstructured":"Johansson M, Dixon L, Bundy A. Dynamic rippling, middle-out reasoning and lemma discovery. In Lecture Notes in Computer Science 6463, Siegler S, Wasser N (eds.), Springer, 2010, pp.102\u2013116. DOI: https:\/\/doi.org\/10.1007\/978-3-642-17172-7_6."},{"issue":"3","key":"6040_CR27","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10817-010-9193-y","volume":"47","author":"M Johansson","year":"2011","unstructured":"Johansson M, Dixon L, Bundy A. Conjecture synthesis for inductive theories. Journal of Automated Reasoning, 2011, 47(3): 251\u2013289. DOI: https:\/\/doi.org\/10.1007\/s10817-010-9193-y.","journal-title":"Journal of Automated Reasoning"},{"key":"6040_CR28","doi-asserted-by":"publisher","first-page":"6000","DOI":"10.5555\/3295222.3295349","volume-title":"Proc. the 31st International Conference on Neural Information Processing Systems","author":"A Vaswani","year":"2017","unstructured":"Vaswani A, Shazeer N, Parmar N, Uszkoreit J, Jones L, Gomez A N, Kaiser L, Polosukhin I. Attention is all you need. In Proc. the 31st International Conference on Neural Information Processing Systems, Dec. 2017, pp.6000\u20136010. DOI: https:\/\/doi.org\/10.5555\/3295222.3295349."},{"key":"6040_CR29","series-title":"Technical Report","volume-title":"Language models are unsupervised multitask learners","author":"A Radford","year":"2019","unstructured":"Radford A, Wu J, Child R, Luan D, Amodei D, Sutskever I. Language models are unsupervised multitask learners. Technical Report, OpenAI, 2019. https:\/\/cdn.openai.com\/better-language-models\/language_models_are_unsu-pervised_multitask_learners.pdf"},{"key":"6040_CR30","doi-asserted-by":"publisher","DOI":"10.5555\/3495724.3495883","volume-title":"Proc. the 34th International Conference on Neural Information Processing Systems","author":"T B Brown","year":"2020","unstructured":"Brown T B, Mann B, Ryder N, Subbiah M, Kaplan J, Dhariwal P, Neelakantan A, Shyam P, Sastry G, Askell A, Agarwal S, Herbert-Voss A, Krueger G, Henighan T, Child R, Ramesh A, Ziegler D M, Wu J, Winter C, Hesse C, Chen M, Sigler E, Litwin M, Gray S, Chess B, Clark J, Berner C, McCandlish S, Radford A, Sutskever I, Amodei D. Language models are few-shot learners. In Proc. the 34th International Conference on Neural Information Processing Systems, Dec. 2020, Article No. 159. DOI: https:\/\/doi.org\/10.5555\/3495724.3495883."},{"key":"6040_CR31","unstructured":"OpenAI. GPT-4 technical report. arXiv: 2303.08774, 2023. https:\/\/arxiv.org\/abs\/2303.08774, Jan. 2026."},{"key":"6040_CR32","doi-asserted-by":"publisher","DOI":"10.5555\/3600270.3602070","volume-title":"Proc. the 36th International Conference on Neural Information Processing Systems","author":"J Wei","year":"2022","unstructured":"Wei J, Wang X, Schuurmans D, Bosma M, Ichter B, Xia F, Chi E H, Le Q V, Zhou D. Chain-of-thought prompting elicits reasoning in large language models. In Proc. the 36th International Conference on Neural Information Processing Systems, Nov. 28-Dec. 9, 2022, Article No. 1800. DOI: https:\/\/doi.org\/10.5555\/3600270.3602070."},{"key":"6040_CR33","doi-asserted-by":"publisher","DOI":"10.5555\/3600270.3602281","volume-title":"Proc. the 36th International Conference on Neural Information Processing Systems","author":"L Ouyang","year":"2022","unstructured":"Ouyang L, Wu J, Jiang X, Almeida D, Wainwright C L, Mishkin P, Zhang C, Agarwal S, Slama K, Ray A, Schulman J, Hilton J, Kelton F, Miller L, Simens M, Askell A, Welinder P, Christiano P, Leike J, Lowe R. Training language models to follow instructions with human feedback. In Proc. the 36th International Conference on Neural Information Processing Systems, Nov. 28-Dec. 9, 2022, Article No. 2011. DOI: https:\/\/doi.org\/10.5555\/3600270.3602281."},{"key":"6040_CR34","doi-asserted-by":"publisher","unstructured":"Chowdhery A, Narang S, Devlin J, Bosma M, Mishra G, Roberts A, Barham P, Chung H W, Sutton C, Gehrmann S, Schuh P, Shi K, Tsvyashchenko S, Maynez J, Rao A, Barnes P, Tay Y, Shazeer N, Prabhakaran V, Reif E, Du N, Hutchinson B, Pope R, Bradbury J, Austin J, Isard M, Gur-Ari G, Yin P, Duke T, Levskaya A, Ghemawat S, Dev S, Michalewski H, Garcia X, Misra V, Robinson K, Fedus L, Zhou D, Ippolito D, Luan D, Lim H, Zoph B, Spiridonov A, Sepassi R, Dohan D, Agrawal S, Omernick M, Dai A M, Pillai T S, Pellat M, Lewkowycz A, Moreira E, Child R, Polozov O, Lee K, Zhou Z, Wang X, Saeta B, Diaz M, Firat O, Catasta M, Wei J, Meier-Hellstern K, Eck D, Dean J, Petrov S, Fiedel N. PaLM: Scaling language modeling with pathways. The Journal of Machine Learning Research, 2023, 24(1): Article No. 240. DOI: https:\/\/doi.org\/10.5555\/3648699.3648939.","DOI":"10.5555\/3648699.3648939"},{"key":"6040_CR35","unstructured":"Touvron H, Lavril T, Izacard G, Martinet X, Lachaux M A, Lacroix T, Rozi\u00e8re B, Goyal N, Hambro E, Azhar F, Rodriguez A, Joulin A, Grave E, Lample G. LLaMA: Open and efficient foundation language models. arXiv: 2302.13971, 2023. https:\/\/arxiv.org\/abs\/2302.13971, Jan. 2026."},{"key":"6040_CR36","unstructured":"Gemini Team Google. Gemini: A family of highly capable multimodal models. arXiv: 2312.11805, 2023. https:\/\/arxiv.org\/abs\/2312.11805, Jan. 2026."},{"key":"6040_CR37","unstructured":"DeepSeek-AI. DeepSeek-v2: A strong, economical, and efficient mixture-of-experts language model. arXiv: 2405.04434, 2024. https:\/\/arxiv.org\/abs\/2405.04434, Jan. 2026."},{"key":"6040_CR38","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"Lecture Notes in Computer Science 449","author":"A Bundy","year":"1990","unstructured":"Bundy A, van Harmelen F, Horn C, Smaill A. The OYSTER-CLAM system. In Lecture Notes in Computer Science 449, Stickel M E (ed.), Springer, 1990, pp.647\u2013648. DOI: https:\/\/doi.org\/10.1007\/3-540-52885-7_123."},{"key":"6040_CR39","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Lecture Notes in Computer Science 2741","author":"L Dixon","year":"2003","unstructured":"Dixon L, Fleuriot J. IsaPlanner: A prototype proof planner in Isabelle. In Lecture Notes in Computer Science 2741, Baader Z (ed.), Springer, 2003, pp.279\u2013283. DOI: https:\/\/doi.org\/10.1007\/978-3-540-45085-6_22."},{"key":"6040_CR40","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-28756-5_28","volume-title":"Lecture Notes in Computer Science 7214","author":"W Sonnex","year":"2012","unstructured":"Sonnex W, Drossopoulou S, Eisenbach S. Zeno: An automated prover for properties of recursive data structures. In Lecture Notes in Computer Science 7214, Flanagan C, K\u00f6nig Z (eds.), Springer, 2012, pp.407\u2013421. DOI: https:\/\/doi.org\/10.1007\/978-3-642-28756-5_28."},{"key":"6040_CR41","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3319-96812-4_19","volume-title":"Lecture Notes in Computer Science 11006","author":"Y Nagashima","year":"2018","unstructured":"Nagashima Y, Parsert J. Goal-oriented conjecturing for Isabelle\/HOL. In Lecture Notes in Computer Science 11006, Rabe F, Farmer W M, Passmore G O, Youssef A (eds.), Springer, 2018, pp.225\u2013231. DOI: https:\/\/doi.org\/10.1007\/978-3319-96812-4_19."},{"key":"6040_CR42","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-030-30048-7_35","volume-title":"Lecture Notes in Computer Science 11802","author":"W Yang","year":"2019","unstructured":"Yang W, Fedyukovich G, Gupta A. Lemma synthesis for automating induction over algebraic data types. In Lecture Notes in Computer Science 11802, Schiex T, de Givry S (eds.), Springer, 2019, pp.600\u2013617. DOI: https:\/\/doi.org\/10.1007\/978-3-030-30048-7_35."},{"issue":"OOPSLA2","key":"6040_CR43","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/3563306","volume":"6","author":"A Sivaraman","year":"2022","unstructured":"Sivaraman A, Sanchez-Stern A, Chen B, Lerner S, Millstein T. Data-driven lemma synthesis for interactive proofs. Proceedings of the ACM on Programming Languages, 2022, 6(OOPSLA2): 143. DOI: https:\/\/doi.org\/10.1145\/3563306.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"6040_CR44","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-031-42441-0_9","volume-title":"Lecture Notes in Computer Science 14155","author":"Y Nagashima","year":"2023","unstructured":"Nagashima Y, Xu Z, Wang N, Goc D S, Bang J. Template-based conjecturing for automated induction in Isabelle\/HOL. In Lecture Notes in Computer Science 14155, Hojjat H, \u00c1brah\u00e1m E (eds.), Springer, 2023, pp.112\u2013125. DOI: https:\/\/doi.org\/10.1007\/978-3-031-42441-0_9."},{"issue":"4","key":"6040_CR45","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B Buchberger","year":"2006","unstructured":"Buchberger B, Cr\u0103ciun A, Jebelean T, Kov\u00e1cs L, Kutsia T, Nakagawa K, Piroi F, Popov N, Robu J, Rosenkranz M, Windsteiger W. Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic, 2006, 4(4): 470\u2013504. DOI: https:\/\/doi.org\/10.1016\/j.jal.2005.10.006.","journal-title":"Journal of Applied Logic"},{"key":"6040_CR46","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Lecture Notes in Computer Science 7898","author":"K Claessen","year":"2013","unstructured":"Claessen K, Johansson M, Ros\u00e9n D, Smallbone N. Automating inductive proofs using theory exploration. In Lecture Notes in Computer Science 7898, Bonacina M P (ed.), Springer, 2013, pp.392\u2013406. DOI: https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27."},{"key":"6040_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.341.1","volume-title":"Proc. the 9th International Workshop on Verification and Program Transformation","author":"M Johansson","year":"2021","unstructured":"Johansson M, Smallbone N. Conjectures, tests and proofs: An overview of theory exploration. In Proc. the 9th International Workshop on Verification and Program Transformation, Mar. 2021, pp.1\u201316. DOI: https:\/\/doi.org\/10.4204\/EPTCS.341.1."},{"key":"6040_CR48","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/3-540-48660-7_37","volume-title":"Lecture Notes in Computer Science 1632","author":"J Zhang","year":"1999","unstructured":"Zhang J. System description: MCS: Model-based conjecture searching. In Lecture Notes in Computer Science 1632, Ganzinger H (ed.), Springer, 1999, pp.393\u2013397. DOI: https:\/\/doi.org\/10.1007\/3-540-48660-7_37."},{"key":"6040_CR49","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/3-540-45620-1_24","volume-title":"Lecture Notes in Computer Science 2392","author":"S Colton","year":"2002","unstructured":"Colton S. The HR program for theorem generation. In Lecture Notes in Computer Science 2392, Voronkov A (ed.), Springer, 2002, pp.285\u2013289. DOI: https:\/\/doi.org\/10.1007\/3-540-45620-1_24."},{"key":"6040_CR50","series-title":"Ph.D. Thesis","volume-title":"AM: An artificial intelligence approach to discovery in mathematics as heuristic search","author":"D B Lenat","year":"1976","unstructured":"Lenat D B. AM: An artificial intelligence approach to discovery in mathematics as heuristic search [Ph.D. Thesis]. Stanford University, Stanford, 1976."},{"key":"6040_CR51","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-64213977-2_3","volume-title":"Lecture Notes in Computer Science 6143","author":"K Claessen","year":"2010","unstructured":"Claessen K, Smallbone N, Hughes J. QuickSpec: Guessing formal specifications using testing. In Lecture Notes in Computer Science 6143, Fraser G, Gargantini A (eds.), Springer, 2010, pp.6\u201321. DOI: https:\/\/doi.org\/10.1007\/978-3-64213977-2_3."},{"key":"6040_CR52","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/351240.351266","volume-title":"Proc. the 5th ACM SIGPLAN International Conference on Functional Programming","author":"K Claessen","year":"2000","unstructured":"Claessen K, Hughes J. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proc. the 5th ACM SIGPLAN International Conference on Functional Programming, Sept. 2000, pp.268\u2013279. DOI: https:\/\/doi.org\/10.1145\/351240.351266."},{"key":"6040_CR53","doi-asserted-by":"publisher","first-page":"e18","DOI":"10.1017\/S0956796817000090","volume":"27","author":"N Smallbone","year":"2017","unstructured":"Smallbone N, Johansson M, Claessen K, Algehed M. Quick specifications for the busy programmer. Journal of Functional Programming, 2017, 27:e18. DOI: https:\/\/doi.org\/10.1017\/S0956796817000090.","journal-title":"Journal of Functional Programming"},{"key":"6040_CR54","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/3462172.3462192","volume-title":"Proc. the 32nd Symposium on Implementation and Application of Functional Languages","author":"S H Einarsd\u00f3ttir","year":"2020","unstructured":"Einarsd\u00f3ttir S H, Smallbone N, Johansson M. Template-based theory exploration: Discovering properties of functional programs by testing. In Proc. the 32nd Symposium on Implementation and Application of Functional Languages, Sept. 2020, pp.67\u201378. DOI: https:\/\/doi.org\/10.1145\/3462172.3462192."},{"key":"6040_CR55","series-title":"Master\u2019s Thesis","volume-title":"Proving equational Haskell properties using automated theorem provers","author":"D Ros\u00e9n","year":"2012","unstructured":"Ros\u00e9n D. Proving equational Haskell properties using automated theorem provers. [Master\u2019s Thesis], University of Gothenburg, G\u00f6teborg, 2012."},{"key":"6040_CR56","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-20615-8_23","volume-title":"Lecture Notes in Computer Science 9150","author":"K Claessen","year":"2015","unstructured":"Claessen K, Johansson M, Ros\u00e9n D, Smallbone N. TIP: Tons of inductive problems. In Lecture Notes in Computer Science 9150, Kerber M, Carette J, Kaliszyk C, Rabe F, Sorge V (eds.), Springer, 2015, pp.333\u2013337. DOI: https:\/\/doi.org\/10.1007\/978-3-319-20615-8_23."},{"key":"6040_CR57","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-31908434-3_9","volume-title":"Lecture Notes in Computer Science 8543","author":"M Johansson","year":"2014","unstructured":"Johansson M, Ros\u00e9n D, Smallbone N, Claessen K. Hipster: Integrating theory exploration in a proof assistant. In Lecture Notes in Computer Science 8543, Watt S M, Davenport J H, Sexton A P, Sojka P, Urban J (eds.), Springer, 2014, pp.108\u2013122. DOI: https:\/\/doi.org\/10.1007\/978-3-31908434-3_9."},{"key":"6040_CR58","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1109\/ICST57152.2023.00035","volume-title":"Proc. the 2023 IEEE Conference on Software Testing, Verification and Validation","author":"M P Gissurarson","year":"2023","unstructured":"Gissurarson M P, Roque D, Koppel J. Spectacular: Finding laws from 25 trillion terms. In Proc. the 2023 IEEE Conference on Software Testing, Verification and Validation, Apr. 2023, pp.293\u2013304. DOI: https:\/\/doi.org\/10.1109\/ICST57152.2023.00035."},{"key":"6040_CR59","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-81688-9_6","volume-title":"Lecture Notes in Computer Science 12760","author":"E Singher","year":"2021","unstructured":"Singher E, Itzhaky S. Theory exploration powered by deductive synthesis. In Lecture Notes in Computer Science 12760, Silva A, Leino K R M (eds.), Springer, 2021, pp.125\u2013148. DOI: https:\/\/doi.org\/10.1007\/978-3-030-81688-9_6."},{"issue":"2","key":"6040_CR60","doi-asserted-by":"publisher","first-page":"1637","DOI":"10.1016\/j.eswa.2011.06.055","volume":"39","author":"O Montano-Rivas","year":"2012","unstructured":"Montano-Rivas O, McCasland R, Dixon L, Bundy A. Scheme-based theorem discovery and concept invention. Expert Systems with Applications, 2012, 39(2): 1637\u20131646. DOI: https:\/\/doi.org\/10.1016\/j.eswa.2011.06.055.","journal-title":"Expert Systems with Applications"},{"key":"6040_CR61","volume-title":"Proc. the 15th Conference on Intelligent Computer Mathematics (CICM 2022) Informal Proceedings","author":"S H Einarsd\u00f3ttir","year":"2022","unstructured":"Einarsd\u00f3ttir S H, Johansson M, Smallbone N. LOL: A library of lemma templates for data-driven conjecturing. In Proc. the 15th Conference on Intelligent Computer Mathematics (CICM 2022) Informal Proceedings, Aug. 2022, Article No. 22."},{"key":"6040_CR62","first-page":"49","volume-title":"Proc. the 19th International Florida Artificial Intelligence Research Society Conference","author":"Y Puzis","year":"2006","unstructured":"Puzis Y, Gao Y, Sutcliffe G. Automated generation of interesting theorems. In Proc. the 19th International Florida Artificial Intelligence Research Society Conference, May 2006, pp.49\u201354."},{"issue":"2","key":"6040_CR63","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G Sutcliffe","year":"1998","unstructured":"Sutcliffe G, Suttner C. The TPTP problem library. Journal of Automated Reasoning, 1998, 21(2): 177\u2013203. DOI: https:\/\/doi.org\/10.1023\/A:1005806324129.","journal-title":"Journal of Automated Reasoning"},{"key":"6040_CR64","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1109\/SYNASC.2006.51","volume-title":"Proc. the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing","author":"R L McCasland","year":"2006","unstructured":"McCasland R L, Bundy A. MATHSAiD: A mathematical theorem discovery tool. In Proc. the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sept. 2006, pp.17\u201322. DOI: https:\/\/doi.org\/10.1109\/SYNASC.2006.51."},{"issue":"3","key":"6040_CR65","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10489-017-0954-8","volume":"47","author":"R L McCasland","year":"2017","unstructured":"McCasland R L, Bundy A, Smith P F. MATHSAiD: Automated mathematical theory exploration. Applied Intelligence, 2017, 47(3): 585\u2013606. DOI: https:\/\/doi.org\/10.1007\/S10489-017-0954-8.","journal-title":"Applied Intelligence"},{"key":"6040_CR66","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2014.06.028","volume":"554","author":"H Gao","year":"2014","unstructured":"Gao H, Goto Y, Cheng J. A systematic methodology for automated theorem finding. Theoretical Computer Science, 2014, 554:2\u201321. DOI: https:\/\/doi.org\/10.1016\/J.TCS.2014.06.028.","journal-title":"Theoretical Computer Science"},{"key":"6040_CR67","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/3-540-48912-6_65","volume-title":"Lecture Notes in Computer Science 1574","author":"J Cheng","year":"1999","unstructured":"Cheng J. A strong relevant logic model of epistemic processes in scientific discovery. In Lecture Notes in Computer Science 1574, Zhong N, Zhou L (eds.), Springer, 1999, pp.489\u2013493. DOI: https:\/\/doi.org\/10.1007\/3-540-48912-6_65."},{"issue":"1\/2","key":"6040_CR68","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/S0004-3702(83)80005-8","volume":"21","author":"D B Lenat","year":"1983","unstructured":"Lenat D B. EURISKO: A program that learns new heuristics and domain concepts: The nature of heuristics III: Program design and results. Artificial Intelligence, 1983, 21(1\/2): 61\u201398. DOI: https:\/\/doi.org\/10.1016\/S0004-3702(83)80005-8.","journal-title":"Artificial Intelligence"},{"issue":"14\/15","key":"6040_CR69","doi-asserted-by":"publisher","first-page":"2010","DOI":"10.1016\/j.artint.2011.07.001","volume":"175","author":"P Tang","year":"2011","unstructured":"Tang P, Lin F. Discovering theorems in game theory: Two-person games with unique pure Nash equilibrium payoffs. Artificial Intelligence, 2011, 175(14\/15): 2010\u20132020. DOI: https:\/\/doi.org\/10.1016\/J.ARTINT.2011.07.001.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"6040_CR70","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1111\/j.1467-8640.1988.tb00089.x","volume":"4","author":"S L Epstein","year":"1988","unstructured":"Epstein S L. Learning and discovery: One system\u2019s search for mathematical knowledge. Computational Intelligence, 1988, 4(1): 42\u201353. DOI: https:\/\/doi.org\/10.1111\/J.1467-8640.1988.TB00089.X.","journal-title":"Computational Intelligence"},{"issue":"1\/2\/3","key":"6040_CR71","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0012-365X(88)90199-9","volume":"72","author":"S Fajtlowicz","year":"1988","unstructured":"Fajtlowicz S. On conjectures of Graffiti. Discrete Mathematics, 1988, 72(1\/2\/3): 113\u2013118. DOI: https:\/\/doi.org\/10.1016\/0012-365X(88)90199-9.","journal-title":"Discrete Mathematics"},{"key":"6040_CR72","doi-asserted-by":"crossref","unstructured":"Davila R. Automated conjecturing in mathematics with TxGraffiti. arXiv: 2409.19379, 2024. https:\/\/arxiv.org\/abs\/2409.19379, Jan. 2026.","DOI":"10.1007\/s10472-026-10005-5"},{"key":"6040_CR73","doi-asserted-by":"publisher","first-page":"85","DOI":"10.4204\/EPTCS.398.12","volume-title":"Proc. the 14th International Conference on Automated Deduction in Geometry","author":"P Quaresma","year":"2023","unstructured":"Quaresma P, Graziani P, Nicoletti S M. Considerations on approaches and metrics in automated theorem generation\/finding in geometry. In Proc. the 14th International Conference on Automated Deduction in Geometry, Sept. 2023, pp.85\u2013100. DOI: https:\/\/doi.org\/10.4204\/EPTCS.398.12."},{"key":"6040_CR74","volume-title":"Mathematics Mechanization: Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving, and Polynomial Equations-Solving","author":"W T Wu","year":"2000","unstructured":"Wu W T. Mathematics Mechanization: Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving, and Polynomial Equations-Solving. Science Press, Kluwer Academic Publishers, 2000."},{"key":"6040_CR75","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1142\/9789812791085_0016","volume-title":"Selected Works of Wen-Tsun Wu","author":"W T Wu","year":"2008","unstructured":"Wu W T. A mechanization method of geometry and its applications: I. Distances, areas and volumes. In Selected Works of Wen-Tsun Wu, Wu W T (ed.), World Scientific, pp.259\u2013271, 2008. DOI: https:\/\/doi.org\/10.1142\/9789812791085_0016."},{"key":"6040_CR76","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-56804-2_39","volume-title":"Lecture Notes in Computer Science 689","author":"R Bagai","year":"1993","unstructured":"Bagai R, Shanbhogue V, \u017bytkow J M, Chou S C. Automatic theorem generation in plane geometry. In Lecture Notes in Computer Science 689, Komorowski J, Ra\u015b Z W (eds.), Springer, 1993, pp.415\u2013424. DOI: https:\/\/doi.org\/10.1007\/3-540-56804-2_39."},{"issue":"2","key":"6040_CR77","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 Communications in Computer Algebra, 2021, 55(2): 39\u201343. DOI: https:\/\/doi.org\/10.1145\/3493492.3493495.","journal-title":"ACM Communications in Computer Algebra"},{"key":"6040_CR78","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-15081-9_7","volume-title":"Computer Algebra and Polynomials: Applications of Algebra and Number Theory","author":"Z Kov\u00e1cs","year":"2015","unstructured":"Kov\u00e1cs Z, Parisse B. Giac and GeoGebra-improved Gr\u00f6bner basis computations. In Computer Algebra and Polynomials: Applications of Algebra and Number Theory, Gutierrez J, Schicho J, Weimann M (eds.), Springer, 2015, pp.126\u2013138. DOI: https:\/\/doi.org\/10.1007\/978-3-319-15081-9_7."},{"issue":"3","key":"6040_CR79","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"S C Chou","year":"2000","unstructured":"Chou S C, Gao X S, Zhang J Z. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 2000, 25(3): 219\u2013246. DOI: https:\/\/doi.org\/10.1023\/A:1006171315513.","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"6040_CR80","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/s10817-021-09591-2","volume":"65","author":"X Peng","year":"2021","unstructured":"Peng X, Chen Q, Zhang J, Chen M. Automated discovery of geometric theorems based on vector equations. Journal of Automated Reasoning, 2021, 65(6): 711\u2013726. DOI: https:\/\/doi.org\/10.1007\/S10817-021-09591-2.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"6040_CR81","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1111\/J.1551-6708.1981.TB00869.X","volume":"5","author":"P Langley","year":"1981","unstructured":"Langley P. Data-driven discovery of physical laws. Cognitive Science, 1981, 5(1): 31\u201354. DOI: https:\/\/doi.org\/10.1111\/J.1551-6708.1981.TB00869.X.","journal-title":"Cognitive Science"},{"issue":"1\/2","key":"6040_CR82","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0012-365X(99)00206-X","volume":"212","author":"G Caporossi","year":"2000","unstructured":"Caporossi G, Hansen P. Variable neighborhood search for extremal graphs: 1 The AutoGraphiX system. Discrete Mathematics, 2000, 212(1\/2): 29\u201344. DOI: https:\/\/doi.org\/10.1016\/S0012-365X(99)00206-X.","journal-title":"Discrete Mathematics"},{"issue":"7844","key":"6040_CR83","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1038\/s41586-021-03229-4","volume":"590","author":"G Raayoni","year":"2021","unstructured":"Raayoni G, Gottlieb S, Manor Y, Pisha G, Harris Y, Mendlovic U, Haviv D, Hadad Y, Kaminer I. Generating conjectures on fundamental constants with the Ramanujan machine. Nature, 2021, 590(7844): 67\u201373. DOI: https:\/\/doi.org\/10.1038\/S41586-021-03229-4.","journal-title":"Nature"},{"issue":"16","key":"6040_CR84","doi-asserted-by":"publisher","first-page":"eaay2631","DOI":"10.1126\/sciadv.aay2631","volume":"6","author":"S M Udrescu","year":"2020","unstructured":"Udrescu S M, Tegmark M. AI Feynman: A physics-inspired method for symbolic regression. Science Advances, 2020, 6(16): eaay2631. DOI: https:\/\/doi.org\/10.1126\/sciadv.aay2631.","journal-title":"Science Advances"},{"issue":"1\/2\/3","key":"6040_CR85","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/S0012-365X(03)00311-X","volume":"276","author":"G Caporossi","year":"2004","unstructured":"Caporossi G, Hansen P. Variable neighborhood search for extremal graphs. 5. Three ways to automate finding conjectures. Discrete Mathematics, 2004, 276(1\/2\/3): 81\u201394. DOI: https:\/\/doi.org\/10.1016\/S0012-365X(03)00311-X.","journal-title":"Discrete Mathematics"},{"issue":"7887","key":"6040_CR86","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1038\/s41586-021-04086-x","volume":"600","author":"A Davies","year":"2021","unstructured":"Davies A, Veli\u010dkovi\u0107 P, Buesing L, Blackwell S, Zheng D, Toma\u0161ev N, Tanburn R, Battaglia P, Blundell C, Juh\u00e1sz A, Lackenby M, Williamson G, Hassabis D, Kohli P. Advancing mathematics by guiding human intuition with AI. Nature, 2021, 600(7887): 70\u201374. DOI: https:\/\/doi.org\/10.1038\/S41586-021-04086-X.","journal-title":"Nature"},{"key":"6040_CR87","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-45221-5_27","volume-title":"Lecture Notes in Computer Science 8312","author":"J Heras","year":"2013","unstructured":"Heras J, Komendantskaya E, Johansson M, Maclean E. Proof-pattern recognition and lemma discovery in ACL2. In Lecture Notes in Computer Science 8312, McMillan K, Middeldorp A, Voronkov A (eds.), Springer, 2013, pp.389\u2013406. DOI: https:\/\/doi.org\/10.1007\/978-3-642-45221-5_27."},{"key":"6040_CR88","doi-asserted-by":"publisher","first-page":"61","DOI":"10.4204\/EPTCS.152.5","volume-title":"Proc. the 12th International Workshop on the ACL2 Theorem Prover and Its Applications","author":"J Heras","year":"2014","unstructured":"Heras J, Komendantskaya E. ACL2(ml): Machine-learning for ACL2. In Proc. the 12th International Workshop on the ACL2 Theorem Prover and Its Applications, Jul. 2014, pp.61\u201375. DOI: https:\/\/doi.org\/10.4204\/EPTCS.152.5."},{"key":"6040_CR89","first-page":"219","volume-title":"Joint Proc. the 2016 FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 Co-Located with the 9th Conference on Intelligent Computer Mathematics","author":"T Gauthier","year":"2016","unstructured":"Gauthier T, Kaliszyk C, Urban J. Initial experiments with statistical conjecturing over large formal corpora. In Joint Proc. the 2016 FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 Co-Located with the 9th Conference on Intelligent Computer Mathematics, Jul. 2016, pp.219\u2013228."},{"key":"6040_CR90","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-0843-3_20","volume-title":"Lecture Notes in Computer Science 8543","author":"T Gauthier","year":"2014","unstructured":"Gauthier T, Kaliszyk C. Matching concepts across HOL libraries. In Lecture Notes in Computer Science 8543, Watt S M, Davenport J H, Sexton A P, Sojka P, Urban J (eds.), Springer, 2014, pp.267\u2013281. DOI: https:\/\/doi.org\/10.1007\/978-3-319-0843-3_20."},{"key":"6040_CR91","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-030-53518-6_24","volume-title":"Lecture Notes in Computer Science 12236","author":"J Urban","year":"2020","unstructured":"Urban J, Jakub\u016fv J. First neural conjecturing datasets and experiments. In Lecture Notes in Computer Science 12236, Benzm\u00fcller C, Miller B (eds.), Springer, 2020, pp.315\u2013323. DOI: https:\/\/doi.org\/10.1007\/978-3-030-53518-6_24."},{"key":"6040_CR92","volume-title":"Proc. the 9th International Conference on Learning Representations","author":"M N Rabe","year":"2021","unstructured":"Rabe M N, Lee D, Bansal K, Szegedy C. Mathematical reasoning via self-supervised skip-tree training. In Proc. the 9th International Conference on Learning Representations, May 2021."},{"key":"6040_CR93","first-page":"454","volume-title":"Proc. the 36th International Conference on Machine Learning","author":"K Bansal","year":"2019","unstructured":"Bansal K, Loos S, Rabe M, Szegedy C, Wilcox S. HOList: An environment for machine learning of higher order logic theorem proving. In Proc. the 36th International Conference on Machine Learning, Jun. 2019, pp.454\u2013463."},{"key":"6040_CR94","first-page":"62","volume-title":"Proc. the 17th International Workshop on Neural-Symbolic Learning and Reasoning","author":"M Johansson","year":"2023","unstructured":"Johansson M, Smallbone N. Exploring mathematical conjecturing with large language models. In Proc. the 17th International Workshop on Neural-Symbolic Learning and Reasoning, Jul. 2023, pp.62\u201377."},{"key":"6040_CR95","doi-asserted-by":"publisher","DOI":"10.52202\/079017-1362","volume-title":"Proc. the 38th International Conference on Neural Information Processing Systems","author":"G Poesia","year":"2024","unstructured":"Poesia G, Broman D, Haber N, Goodman N D. Learning formal mathematics from intrinsic motivation. In Proc. the 38th International Conference on Neural Information Processing Systems, Dec. 2024, Article No. 1362. DOI: https:\/\/doi.org\/10.52202\/079017-1362."},{"key":"6040_CR96","unstructured":"Alhessi Y, Einarsd\u00f3ttir S H, Granberry G, First E, Johansson M, Lerner S, Smallbone N. Lemmanaid: Neuro-symbolic lemma conjecturing. arXiv: 2504.04942, 2025. https:\/\/arxiv.org\/abs\/2504.04942, Jan. 2026."},{"key":"6040_CR97","first-page":"20212","volume-title":"Proc. the 12th International Conference on Learning Representations","author":"H Wang","year":"2024","unstructured":"Wang H, Xin H, Zheng C, Liu Z, Cao Q, Huang Y, Xiong J, Shi H, Xie E, Yin J, Li Z, Liang X. LEGO-prover: Neural theorem proving with growing libraries. In Proc. the 12th International Conference on Learning Representations, May 2024, pp.20212\u201320243."},{"key":"6040_CR98","first-page":"1","volume-title":"Proc. the 11th International Conference on Learning Representations","author":"A Q Jiang","year":"2023","unstructured":"Jiang A Q, Welleck S, Zhou J P, Li W, Liu J, Jamnik M, Lacroix T, Lample G, Wu Y. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In Proc. the 11th International Conference on Learning Representations, May 2023, pp.1\u201319."},{"key":"6040_CR99","unstructured":"Cao C, Song L, Li Z, Le X, Zhang X, Xue H, Yang F. Reviving DSP for advanced theorem proving in the era of reasoning models. arXiv: 2506.11487, 2025. https:\/\/arxiv.org\/abs\/2506.11487, Jan. 2026."},{"key":"6040_CR100","doi-asserted-by":"publisher","DOI":"10.52202\/079017-2753","volume-title":"Proc. the 38th International Conference on Neural Information Processing Systems","author":"H Wang","year":"2024","unstructured":"Wang H, Xin H, Liu Z, Li W, Huang Y, Lu J, Yang Z, Tang J, Yin J, Li Z, Liang X. Proving theorems recursively. In Proc. the 38th International Conference on Neural Information Processing Systems, Dec. 2024, Article No. 2753. DOI: https:\/\/doi.org\/10.52202\/079017-2753."},{"key":"6040_CR101","unstructured":"Xin R, Zheng Z, Nie Y, Yuan K, Xiao X. Scaling up multi-turn off-policy RL and multi-agent tree search for LLM step-provers. arXiv: 2509.06493, 2025. https:\/\/arxiv.org\/abs\/2509.06493, Jan. 2026."},{"key":"6040_CR102","unstructured":"Ren Z Z, Shao Z, Song J, Xin H, Wang H, Zhao W, Zhang L, Fu Z, Zhu Q, Yang D, Wu Z F, Gou Z, Ma S, Tang H, Liu Y, Gao W, Guo D, Ruan C. DeepSeek-prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv: 2504.21801, 2025. https:\/\/arxiv.org\/abs\/2504.21801, Jan. 2026."},{"key":"6040_CR103","unstructured":"Zhou Y, Zhao J, Zhang Y, Wang B, Wang S, Chen L, Wang J, Chen H, Jie A, Zhang X, Wang H, Trung L, Ye R, Hoang P N, Zhang H, Sun P, Li H. Solving formal math problems by decomposition and iterative reflection. arXiv: 2507.15225, 2025. https:\/\/arxiv.org\/abs\/2504.21801, Jan. 2026."},{"key":"6040_CR104","unstructured":"Chen L, Gu J, Huang L, Huang W, Jiang Z, Jie A, Jin X, Jin X, Li C, Ma K, Ren C, Shen J, Shi W, Sun T, Sun H, Wang J, Wang S, Wang Z, Wei C, Wei S, Wu Y, Wu Y, Xia Y, Xin J, Yang F, Ying H, Yuan H, Yuan Z, Zhan T, Zhang C, Zhang Y, Zhang G, Zhao T, Zhao J, Zhou Y, Zhu T H. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv: 2507.23726, 2025. https:\/\/arxiv.org\/abs\/2507.23726, Jan. 2026."},{"key":"6040_CR105","unstructured":"Wang H, Unsal M, Lin X, Baksys M, Liu J, Dos Santos M, Sung F, Vinyes M, Ying Z, Zhu Z, Lu J, de Saxc\u00e9 H, Bailey B, Song C, Xiao C, Zhang D, Zhang E, Pu F, Zhu H, Liu J, Bayer J, Michel J, Yu L, Dreyfus-Schmidt L, Tunstall L, Pagani L, Machado M, Bourigault P, Wang R, Polu S, Barroyer T, Li W D, Niu Y, Fleureau Y, Hu Y, Yu Z, Wang Z, Yang Z, Liu Z, Li J. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv: 2504.11354, 2025. https:\/\/arxiv.org\/abs\/2504.11354, Jan. 2026."},{"key":"6040_CR106","unstructured":"Shang S, Wan R, Peng Y, Wu Y, Chen X H, Yan J, Zhang X. StepFun-prover preview: Let\u2019s think and verify step by step. arXiv: 2507.20199, 2025. https:\/\/arxiv.org\/abs\/2507.20199, Jan. 2026."},{"key":"6040_CR107","unstructured":"Lin Y, Tang S, Lyu B, Yang Z, Chung J H, Zhao H, Jiang L, Geng Y, Ge J, Sun J, Wu J, Gesi J, Lu X, Acuna D, Yang K, Lin H, Choi Y, Chen D, Arora S, Jin C. Goedel-prover-V2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv: 2508.03613, 2025. https:\/\/arxiv.org\/abs\/2508.03613, Jan. 2026."},{"key":"6040_CR108","unstructured":"Firoiu V, Aygun E, Anand A, Ahmed Z, Glorot X, Orseau L, Zhang L, Precup D, Mourad S. Training a first-order theorem prover from synthetic data. arXiv: 2103.03798, 2021. https:\/\/arxiv.org\/abs\/2103.03798, Jan. 2026."},{"key":"6040_CR109","doi-asserted-by":"publisher","DOI":"10.5555\/3495724.3497247","volume-title":"Proc. the 34th International Conference on Neural Information Processing Systems","author":"M Wang","year":"2020","unstructured":"Wang M, Deng J. Learning to prove theorems by learning to generate theorems. In Proc. the 34th International Conference on Neural Information Processing Systems, Dec. 2020, Article No. 1523. DOI: https:\/\/doi.org\/10.5555\/3495724.3497247."},{"key":"6040_CR110","volume-title":"Proc. the 9th International Conference on Learning Representations","author":"Y Wu","year":"2021","unstructured":"Wu Y, Jiang A Q, Ba J, Grosse R. INT: An inequality benchmark for evaluating generalization in theorem proving. In Proc. the 9th International Conference on Learning Representations, May 2021."},{"issue":"7995","key":"6040_CR111","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1038\/s41586-023-06747-5","volume":"625","author":"T H Trinh","year":"2024","unstructured":"Trinh T H, Wu Y, Le Q V, He H, Luong T. Solving olympiad geometry without human demonstrations. Nature, 2024, 625(7995): 476\u2013482. DOI: https:\/\/doi.org\/10.1038\/S41586-023-06747-5.","journal-title":"Nature"},{"key":"6040_CR112","doi-asserted-by":"publisher","DOI":"10.5555\/3737916.3740549","volume-title":"Proc. the 38th International Conference on Neural Information Processing Systems","author":"C Wei","year":"2024","unstructured":"Wei C, Sun M, Wang W. Proving Olympiad algebraic inequalities without human demonstrations. In Proc. the 38th International Conference on Neural Information Processing Systems, Dec. 2024, Article No. 2633. DOI: https:\/\/doi.org\/10.5555\/3737916.3740549."},{"key":"6040_CR113","volume-title":"Proc. the 13th International Conference on Learning Representations","author":"S Wu","year":"2025","unstructured":"Wu S, Lu S, Gong Y, Duan N, Wei P. Alchemy: Amplifying theorem-proving capability through symbolic mutation. In Proc. the 13th International Conference on Learning Representations, Apr. 2025."},{"key":"6040_CR114","unstructured":"Onda N, Kasaura K, Oriike Y, Taniguchi M, Sannai A, Sonoda S. LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving. arXiv: 2506.22005, 2025. https:\/\/arxiv.org\/abs\/2506.22005, Jan. 2026."},{"key":"6040_CR115","first-page":"14114","volume-title":"Proc. the 42nd International Conference on Machine Learning","author":"K Dong","year":"2025","unstructured":"Dong K, Ma T. STP: Self-play LLM theorem provers with iterative conjecturing and proving. In Proc. the 42nd International Conference on Machine Learning, Jul. 2025, pp.14114\u201314136."},{"key":"6040_CR116","doi-asserted-by":"publisher","first-page":"4465","DOI":"10.18653\/v1\/2024.findings-naacl.279","volume-title":"Proc. the 2024 Findings of the Association for Computational Linguistics: NAACL","author":"X Lin","year":"2024","unstructured":"Lin X, Cao Q, Huang Y, Yang Z, Liu Z, Li Z, Liang X. ATG: Benchmarking automated theorem generation for generative language models. In Proc. the 2024 Findings of the Association for Computational Linguistics: NAACL, Jun. 2024, pp.4465\u20134480. DOI: https:\/\/doi.org\/10.18653\/V1\/2024.FINDINGS-NAACL.279."},{"key":"6040_CR117","first-page":"51382","volume-title":"Proc. the 12th International Conference on Learning Representations","author":"J P Zhou","year":"2024","unstructured":"Zhou J P, Wu Y, Li Q, Grosse R. REFACTOR: Learning to extract theorems from proofs. In Proc. the 12th International Conference on Learning Representations, May 2024, pp.51382\u201351402. https:\/\/proceedings.iclr.cc\/paper_files\/paper\/2024\/file\/b21ae5a5df83632324b61b595ab653b9-Paper-Conference.pdf"},{"issue":"3","key":"6040_CR118","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 interest-ingness in automated mathematical discovery. International Journal of Human-Computer Studies, 2000, 53(3): 351\u2013375. DOI: https:\/\/doi.org\/10.1006\/IJHC.2000.0394.","journal-title":"International Journal of Human-Computer Studies"},{"key":"6040_CR119","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1109\/SEFM.2004.10049","volume-title":"Proc. the 2nd International Conference on Software Engineering and Formal Methods","author":"S Berghofer","year":"2004","unstructured":"Berghofer S, Nipkow T. Random testing in Isabelle\/HOL. In Proc. the 2nd International Conference on Software Engineering and Formal Methods, Sept. 2004, pp.230\u2013239. DOI: https:\/\/doi.org\/10.1109\/SEFM.2004.10049."},{"key":"6040_CR120","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.artint.2015.10.002","volume":"231","author":"C E Larson","year":"2016","unstructured":"Larson C E, Van Cleemput N. Automated conjecturing I: Fajtlowicz\u2019s Dalmatian heuristic revisited. Artificial Intelligence, 2016, 231:17\u201338. DOI: https:\/\/doi.org\/10.1016\/j.artint.2015.10.002.","journal-title":"Artificial Intelligence"},{"key":"6040_CR121","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1109\/ICEI.2019.00069","volume-title":"Proc. the 2019 IEEE International Conference on Energy Internet","author":"H Gao","year":"2019","unstructured":"Gao H, Li J, Cheng J. Measuring interestingness of theorems in automated theorem finding by forward reasoning based on strong relevant logic. In Proc. the 2019 IEEE International Conference on Energy Internet, May 2019, pp.356\u2013361. DOI: https:\/\/doi.org\/10.1109\/ICEI.2019.00069."},{"key":"6040_CR122","first-page":"5223","volume-title":"Proc. the 10th International Conference on Learning Representations","author":"K Zheng","year":"2022","unstructured":"Zheng K, Han J M, Polu S. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. In Proc. the 10th International Conference on Learning Representations, Apr. 2022, pp.5223\u20135233."},{"key":"6040_CR123","unstructured":"Azerbayev Z, Piotrowski B, Schoelkopf H, Ayers E W, Radev D, Avigad J. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv: 2302.12433, 2023. https:\/\/arxiv.org\/abs\/2302.12433, Jan. 2026."},{"key":"6040_CR124","doi-asserted-by":"publisher","DOI":"10.52202\/079017-0368","volume-title":"Proc. the 38th International Conference on Neural Information Processing Systems","author":"G Tsoukalas","year":"2024","unstructured":"Tsoukalas G, Lee J, Jennings J, Xin J, Ding M, Jennings M, Thakur A, Chaudhuri S. PUTNAMBENCH: Evaluating neural theorem-provers on the Putnam mathematical competition. In Proc. the 38th International Conference on Neural Information Processing Systems, Dec. 2024, Article No. 368. DOI: https:\/\/doi.org\/10.52202\/079017-0368."},{"key":"6040_CR125","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-031-63498-7_13","volume-title":"Lecture Notes in Computer Science 14739","author":"S H Einarsd\u00f3ttir","year":"2024","unstructured":"Einarsd\u00f3ttir S H, Hajdu M, Johansson M, Smallbone N, Suda M. Lemma discovery and strategies for automated induction. In Lecture Notes in Computer Science 14739, Benzm\u00fcller C, Heule M J H, Schmidt R A (eds.), Springer, 2024, pp.214\u2013232. DOI: https:\/\/doi.org\/10.1007\/978-3-031-63498-7_13."},{"key":"6040_CR126","volume-title":"Metamath: A Computer Language for Mathematical Proofs","author":"N Megill","year":"2019","unstructured":"Megill N, Wheeler D A. Metamath: A Computer Language for Mathematical Proofs. Lulu.com, 2019."},{"key":"6040_CR127","first-page":"6984","volume-title":"Proc. the 36th International Conference on Machine Learning","author":"K Yang","year":"2019","unstructured":"Yang K, Deng J. Learning to prove theorems via interacting with proof assistants. In Proc. the 36th International Conference on Machine Learning, Jun. 2019, pp.6984\u20136994."},{"key":"6040_CR128","first-page":"378","volume-title":"Proc. the 6th Conference on Artificial Intelligence and Theorem Proving","author":"A Q Jiang","year":"2021","unstructured":"Jiang A Q, Li W, Han J M, Wu Y. LISA: Language models of Isabelle proofs. In Proc. the 6th Conference on Artificial Intelligence and Theorem Proving, Sept. 2021, pp.378\u2013392."},{"key":"6040_CR129","doi-asserted-by":"publisher","DOI":"10.52202\/079017-1742","volume-title":"Proc. the 38th International Conference on Neural Information Processing Systems","author":"X Lin","year":"2024","unstructured":"Lin X, Cao Q, Huang Y, Wang H, Lu J, Liu Z, Song L, Liang X. FVEL: Interactive formal verification environment with large language models via theorem proving. In Proc. the 38th International Conference on Neural Information Processing Systems, Dec. 2024, Article No. 1742. DOI: https:\/\/doi.org\/10.52202\/079017-1742."},{"key":"6040_CR130","doi-asserted-by":"publisher","DOI":"10.5555\/3666122.3667066","volume-title":"Proc. the 37th International Conference on Neural Information Processing Systems","author":"K Yang","year":"2023","unstructured":"Yang K, Swope A M, Gu A, Chalamala R, Song P, Yu S, Godil S, Prenger R, Anandkumar A. LeanDojo: Theorem proving with retrieval-augmented language models. In Proc. the 37th International Conference on Neural Information Processing Systems, Dec. 2023, Article No. 944. DOI: https:\/\/doi.org\/10.5555\/3666122.3667066."},{"key":"6040_CR131","unstructured":"Wu Z, Wang J, Lin D, Chen K. LEAN-GitHub: Compiling GitHub Lean repositories for a versatile lean prover. arXiv: 2407.17227, 2024. https:\/\/arxiv.org\/abs\/2407.17227, Jan. 2026."},{"key":"6040_CR132","unstructured":"Li J, Beeching E, Tunstall L, Lipkin B, Soletskyi R, Huang S C, Rasul K, Yu L, Jiang A, Shen Z, Qin Z, Dong B, Zhou L, Fleureau Y, Lample G, Polu S. Numinamath. 2024. https:\/\/github.com\/project-numina\/aimo-progress-prize, January 2026."},{"key":"6040_CR133","doi-asserted-by":"publisher","first-page":"28601","DOI":"10.1609\/AAAI.V39I27.35084","volume-title":"Proc. the 39th AAAI Conference on Artificial Intelligence","author":"C K Reddy","year":"2025","unstructured":"Reddy C K, Shojaee P. Towards scientific discovery with generative AI: Progress, opportunities, and challenges. In Proc. the 39th AAAI Conference on Artificial Intelligence, Feb. 25-Mar. 4, 2025, pp.28601\u201328609. DOI: https:\/\/doi.org\/10.1609\/AAAI.V39I27.35084."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-026-6040-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11390-026-6040-0","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-026-6040-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T09:02:26Z","timestamp":1777107746000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11390-026-6040-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1]]},"references-count":133,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1]]}},"alternative-id":["6040"],"URL":"https:\/\/doi.org\/10.1007\/s11390-026-6040-0","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1]]},"assertion":[{"value":"16 October 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Conflict of Interest\n                      Jian Zhang is an editorial board member for Journal of Computer Science and Technology and was not involved in the editorial review of this article. The authors declare that there are no other competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics"}}]}}