{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:05:31Z","timestamp":1750089931887,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T00:00:00Z","timestamp":1643500800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T00:00:00Z","timestamp":1643500800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Vidi.189.037"],"award-info":[{"award-number":["016.Vidi.189.037"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1007\/s10817-021-09611-1","type":"journal-article","created":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T00:03:06Z","timestamp":1643500986000},"page":"215-238","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Bi-Directional Extensible Interface Between Lean and Mathematica"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5266-1121","authenticated-orcid":false,"given":"Robert Y.","family":"Lewis","sequence":"first","affiliation":[]},{"given":"Minchao","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,30]]},"reference":[{"key":"9611_CR1","doi-asserted-by":"crossref","unstructured":"Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., Owre, S.: Computer algebra meets automated theorem proving: integrating Maple and PVS. In: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs \u201901, pp. 27\u201342. Springer-Verlag, London, UK, UK (2001). http:\/\/dl.acm.org\/citation.cfm?id=646528.695189","DOI":"10.1007\/3-540-44755-5_4"},{"key":"9611_CR2","doi-asserted-by":"publisher","unstructured":"Ayers, E.W., Jamnik, M., Gowers, W.T.: A Graphical user interface framework for formal verification. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021), Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 4:1\u20134:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.4. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13899","DOI":"10.4230\/LIPIcs.ITP.2021.4"},{"issue":"6","key":"9611_CR3","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1080\/00029890.2006.11920330","volume":"113","author":"DH Bailey","year":"2006","unstructured":"Bailey, D.H., Borwein, J.M., Kapoor, V., Weisstein, E.W.: Ten problems in experimental mathematics. Am. Math. Mon. 113(6), 481\u2013509 (2006)","journal-title":"Am. Math. Mon."},{"key":"9611_CR4","doi-asserted-by":"publisher","unstructured":"Ballarin, C., Homann, K., Calmet, J.: Theorems and algorithms: an interface between Isabelle and Maple. In: Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201995, pp. 150\u2013157. ACM, New York, NY, USA (1995). https:\/\/doi.org\/10.1145\/220346.220366","DOI":"10.1145\/220346.220366"},{"key":"9611_CR5","doi-asserted-by":"crossref","unstructured":"Ballarin, C., Paulson, L.C.: A pragmatic approach to extending provers by computer algebra. Fund. Inform. 39(1\u20132), 1\u201320 (1999). Symbolic computation and related topics in artificial intelligence (Plattsburg, NY, 1998)","DOI":"10.3233\/FI-1999-391201"},{"issue":"3","key":"9611_CR6","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1023\/A:1006079212546","volume":"21","author":"A Bauer","year":"1998","unstructured":"Bauer, A., Clarke, E., Zhao, X.: Analytica\u2014an experiment in combining theorem proving and symbolic computation. J. Autom. Res. 21(3), 295\u2013325 (1998). https:\/\/doi.org\/10.1023\/A:1006079212546","journal-title":"J. Autom. Res."},{"key":"9611_CR7","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F Besson","year":"2007","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs, pp. 48\u201362. Springer, Berlin (2007)"},{"key":"9611_CR8","doi-asserted-by":"crossref","unstructured":"Blanchette, J., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. Interactive Theorem Proving, pp. 131\u2013146 (2010)","DOI":"10.1007\/978-3-642-14052-5_11"},{"issue":"1","key":"9611_CR9","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reason."},{"issue":"3\u20134","key":"9611_CR10","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1006\/jsco.1996.0125","volume":"24","author":"W Bosma","year":"1997","unstructured":"Bosma, W., Cannon, J., Playoust, C.: The magma algebra system i: the user language. J. Symb. Comput. 24(3\u20134), 235\u2013265 (1997). https:\/\/doi.org\/10.1006\/jsco.1996.0125","journal-title":"J. Symb. Comput."},{"key":"9611_CR11","doi-asserted-by":"crossref","unstructured":"Bronstein, M.: it-a strongly-typed embeddable computer algebra library. In: International Symposium on Design and Implementation of Symbolic Computation Systems, pp. 22\u201333. Springer (1996)","DOI":"10.1007\/3-540-61697-7_2"},{"issue":"1","key":"9611_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.6092\/issn.1972-5787\/4568","volume":"9","author":"B Buchberger","year":"2016","unstructured":"Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0: computer-assisted natural-style mathematics. J. Formaliz. Reason. 9(1), 149\u2013185 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4568","journal-title":"J. Formaliz. Reason."},{"issue":"2","key":"9611_CR13","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/333104.333110","volume":"6","author":"O Caprotti","year":"1999","unstructured":"Caprotti, O., Carlisle, D.: Openmath and mathml: semantic markup for mathematics. XRDS 6(2), 11\u201314 (1999). https:\/\/doi.org\/10.1145\/333104.333110","journal-title":"XRDS"},{"key":"9611_CR14","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-08970-6_11","volume-title":"Interactive Theorem Proving","author":"F Chyzak","year":"2014","unstructured":"Chyzak, F., Mahboubi, A., Sibut-Pinote, T., Tassi, E.: A computer-algebra-based formal proof of the irrationality of $$\\zeta $$(3). In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving, pp. 160\u2013176. Springer International Publishing, Cham (2014)"},{"issue":"2\u20133","key":"9611_CR15","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inform. Comput. 76(2\u20133), 95\u2013120 (1988). https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3","journal-title":"Inform. Comput."},{"key":"9611_CR16","doi-asserted-by":"publisher","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: COLOG-88 (Tallinn, 1988), Lecture Notes in Computer Science, vol. 417, pp. 50\u201366. Springer, Berlin (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_47","DOI":"10.1007\/3-540-52335-9_47"},{"key":"9611_CR17","unstructured":"Daly, T.: Axiom: The 30 year horizon. Lulu Incorporated (2005)"},{"issue":"5","key":"9611_CR18","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1016\/j.jsc.2004.12.004","volume":"39","author":"D Delahaye","year":"2005","unstructured":"Delahaye, D., Mayero, M.: Dealing with algebraic expressions over a field in Coq using Maple. J. Symb. Comput. 39(5), 569\u2013592 (2005). https:\/\/doi.org\/10.1016\/j.jsc.2004.12.004","journal-title":"J. Symb. Comput."},{"key":"9611_CR19","doi-asserted-by":"publisher","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Interactive theorem proving, Lecture Notes in Computer Science, vol. 7406, pp. 83\u201398. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_7","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"9611_CR20","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-030-53518-6_16","volume-title":"Intelligent Computer Mathematics","author":"F van Doorn","year":"2020","unstructured":"van Doorn, F., Ebner, G., Lewis, R.Y.: Maintaining a library of formal mathematics. In: Benzm\u00fcller, C., Miller, B. (eds.) Intelligent Computer Mathematics, pp. 251\u2013267. Springer International Publishing, Cham (2020)"},{"issue":"ICFP","key":"9611_CR21","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/3110278","volume":"1","author":"G Ebner","year":"2017","unstructured":"Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1(ICFP), 34 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"9611_CR22","doi-asserted-by":"publisher","unstructured":"Ford, I.: Semantic representation of general topology in the Wolfram Language. In: H.\u00a0Geuvers, M.\u00a0England, O.\u00a0Hasan, F.\u00a0Rabe, O.\u00a0Teschke (eds.) Intelligent Computer Mathematics\u201410th International Conference, CICM 2017, Edinburgh, UK, July 17\u201321, Proceedings, Lecture Notes in Computer Science (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_12","DOI":"10.1007\/978-3-319-62075-6_12"},{"issue":"5","key":"9611_CR23","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1016\/j.jsc.2004.12.005","volume":"39","author":"H Gottliebsen","year":"2005","unstructured":"Gottliebsen, H., Kelsey, T., Martin, U.: Hidden verification for computational mathematics. J. Symb. Comput. 39(5), 539\u2013567 (2005). https:\/\/doi.org\/10.1016\/j.jsc.2004.12.005","journal-title":"J. Symb. Comput."},{"issue":"3","key":"9611_CR24","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10817-015-9338-0","volume":"55","author":"J Harrison","year":"2015","unstructured":"Harrison, J.: Formal proofs of hypergeometric sums. J. Autom. Reason. 55(3), 223\u2013243 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9338-0","journal-title":"J. Autom. Reason."},{"key":"9611_CR25","doi-asserted-by":"publisher","unstructured":"Harrison, J., Th\u00e9ry, L.: A skeptic\u2019s approach to combining HOL and Maple. J. Autom. Reason. 21(3), 279\u2013294 (1998). https:\/\/doi.org\/10.1023\/A:1006023127567","DOI":"10.1023\/A:1006023127567"},{"key":"9611_CR26","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Proceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference, Calculemus \u201907 \/ MKM \u201907, pp. 94\u2013105. Springer-Verlag, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73086-6_8","DOI":"10.1007\/978-3-540-73086-6_8"},{"issue":"3","key":"9611_CR27","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1023\/A:1006059810729","volume":"21","author":"M Kerber","year":"1998","unstructured":"Kerber, M., Kohlhase, M., Sorge, V.: Integrating computer algebra into proof planning. J. Autom. Reason. 21(3), 327\u2013355 (1998). https:\/\/doi.org\/10.1023\/A:1006059810729","journal-title":"J. Autom. Reason."},{"key":"9611_CR28","doi-asserted-by":"publisher","unstructured":"Lewis, R.Y.: An extensible ad hoc interface between Lean and Mathematica. In: C.\u00a0Dubois, B.W. Paleo (eds.) Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras\u00edlia, Brazil, 23-24 September 2017, EPTCS, vol. 262, pp. 23\u201337 (2017). https:\/\/doi.org\/10.4204\/EPTCS.262.4","DOI":"10.4204\/EPTCS.262.4"},{"key":"9611_CR29","unstructured":"Mahboubi, A., Sibut-Pinote, T.: A formal proof of the irrationality of $$\\zeta $$(3). Log. Methods Comput. Sci. 17(1) (2021). https:\/\/lmcs.episciences.org\/7193"},{"key":"9611_CR30","doi-asserted-by":"publisher","unstructured":"The mathlib Community: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, p. 367\u2013381. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"9611_CR31","doi-asserted-by":"publisher","unstructured":"McBride, C., McKinna, J.: Functional pearl: I am not a number\u2014I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell \u201904, pp. 1\u20139. ACM, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/1017472.1017477","DOI":"10.1145\/1017472.1017477"},{"key":"9611_CR32","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9611_CR33","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25, pp. 378\u2013388. Springer International Publishing, Cham (2015)"},{"key":"9611_CR34","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction - CADE 28","author":"L de Moura","year":"2021","unstructured":"de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28, pp. 625\u2013635. Springer International Publishing, Cham (2021)"},{"issue":"3","key":"9611_CR35","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1137\/0204018","volume":"4","author":"VR Pratt","year":"1975","unstructured":"Pratt, V.R.: Every prime has a succinct certificate. SIAM J. Comput. 4(3), 214\u2013220 (1975)","journal-title":"SIAM J. Comput."},{"key":"9611_CR36","doi-asserted-by":"crossref","unstructured":"Rabe, F.: The MMT API: a generic MKM system. In: International Conference on Intelligent Computer Mathematics, pp. 339\u2013343. Springer (2013)","DOI":"10.1007\/978-3-642-39320-4_25"},{"key":"9611_CR37","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley-Interscience Series in Discrete Mathematics. John Wiley & Sons Ltd., Chichester. A Wiley-Interscience Publication (1986)"},{"key":"9611_CR38","doi-asserted-by":"publisher","unstructured":"Seddiki, O., Dunchev, C., Khan-Afshar, S., Tahar, S.: Enabling Symbolic and Numerical Computations in HOL Light, pp. 353\u2013358. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_27","DOI":"10.1007\/978-3-319-20615-8_27"},{"key":"9611_CR39","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-030-51054-1_10","volume-title":"Automated Reasoning","author":"S Ullrich","year":"2020","unstructured":"Ullrich, S., de Moura, L.: Beyond notations: Hygienic macro expansion for theorem proving languages. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning, pp. 167\u2013182. Springer International Publishing, Cham (2020)"},{"key":"9611_CR40","doi-asserted-by":"crossref","unstructured":"Williams, H.: Fourier\u2019s method of linear programming and its dual. The American Mathematical Monthly 93(9), 681\u2013695 (1986)","DOI":"10.1080\/00029890.1986.11971923"},{"key":"9611_CR41","unstructured":"Wolfram, S.: An Elementary Introduction to the Wolfram Language. Wolfram Media, Incorporated (2015). https:\/\/books.google.com\/books?id=efIvjgEACAAJ"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09611-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09611-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09611-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,9]],"date-time":"2022-04-09T08:09:57Z","timestamp":1649491797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09611-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,30]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["9611"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09611-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,1,30]]},"assertion":[{"value":"19 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 October 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 January 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}