Top

Journal of Automated Reasoning

Published in:

30-01-2022

A Bi-Directional Extensible Interface Between Lean and Mathematica

Authors: Robert Y. Lewis, Minchao Wu

Published in: Journal of Automated Reasoning | Issue 2/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other and providing a flexible interface for extending translation, our connection allows for the exchange of arbitrary information between the two systems. We show how to make use of the Lean metaprogramming framework to verify certain Mathematica computations, so that the rigor of the proof assistant is not compromised. We also use Mathematica as an untrusted oracle to guide proof search in the proof assistant and interact with a Mathematica notebook from within a Lean session. In the other direction, we import and process Lean declarations from within Mathematica. The proof assistant library serves as a database of mathematical knowledge that the CAS can display and explore.

previous article A Coq Formalization of Lebesgue Integration of Nonnegative Functions

next article Analyzing Read-Once Cutting Plane Proofs in Horn Systems

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

https://robertylewis.com/leanmm/.

https://observablehq.com/@bryangingechen/hello-lean-prover.

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 ’01, pp. 27–42. Springer-Verlag, London, UK, UK (2001). http://dl.acm.org/citation.cfm?id=646528.695189

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–4:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021). https://doi.org/10.4230/LIPIcs.ITP.2021.4. https://drops.dagstuhl.de/opus/volltexte/2021/13899

Bailey, D.H., Borwein, J.M., Kapoor, V., Weisstein, E.W.: Ten problems in experimental mathematics. Am. Math. Mon. 113(6), 481–509 (2006)MathSciNetCrossRef

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 ’95, pp. 150–157. ACM, New York, NY, USA (1995). https://doi.org/10.1145/220346.220366

Ballarin, C., Paulson, L.C.: A pragmatic approach to extending provers by computer algebra. Fund. Inform. 39(1–2), 1–20 (1999). Symbolic computation and related topics in artificial intelligence (Plattsburg, NY, 1998)

Bauer, A., Clarke, E., Zhao, X.: Analytica—an experiment in combining theorem proving and symbolic computation. J. Autom. Res. 21(3), 295–325 (1998). https://doi.org/10.1023/A:1006079212546MathSciNetCrossRefMATH

Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs, pp. 48–62. Springer, Berlin (2007)CrossRef

Blanchette, J., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. Interactive Theorem Proving, pp. 131–146 (2010)

Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)MathSciNetMATH

10.

Bosma, W., Cannon, J., Playoust, C.: The magma algebra system i: the user language. J. Symb. Comput. 24(3–4), 235–265 (1997). https://doi.org/10.1006/jsco.1996.0125MathSciNetCrossRefMATH

11.

Bronstein, M.: it-a strongly-typed embeddable computer algebra library. In: International Symposium on Design and Implementation of Symbolic Computation Systems, pp. 22–33. Springer (1996)

12.

Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0: computer-assisted natural-style mathematics. J. Formaliz. Reason. 9(1), 149–185 (2016). https://doi.org/10.6092/issn.1972-5787/4568MathSciNetCrossRefMATH

13.

Caprotti, O., Carlisle, D.: Openmath and mathml: semantic markup for mathematics. XRDS 6(2), 11–14 (1999). https://doi.org/10.1145/333104.333110CrossRef

14.

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–176. Springer International Publishing, Cham (2014)CrossRef

15.

Coquand, T., Huet, G.: The calculus of constructions. Inform. Comput. 76(2–3), 95–120 (1988). https://doi.org/10.1016/0890-5401(88)90005-3MathSciNetCrossRefMATH

16.

Coquand, T., Paulin, C.: Inductively defined types. In: COLOG-88 (Tallinn, 1988), Lecture Notes in Computer Science, vol. 417, pp. 50–66. Springer, Berlin (1990). https://doi.org/10.1007/3-540-52335-9_47

17.

Daly, T.: Axiom: The 30 year horizon. Lulu Incorporated (2005)

18.

Delahaye, D., Mayero, M.: Dealing with algebraic expressions over a field in Coq using Maple. J. Symb. Comput. 39(5), 569–592 (2005). https://doi.org/10.1016/j.jsc.2004.12.004MathSciNetCrossRefMATH

19.

Dénès, M., Mörtberg, 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–98. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_7

20.

van Doorn, F., Ebner, G., Lewis, R.Y.: Maintaining a library of formal mathematics. In: Benzmüller, C., Miller, B. (eds.) Intelligent Computer Mathematics, pp. 251–267. Springer International Publishing, Cham (2020)CrossRef

21.

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)CrossRef

22.

Ford, I.: Semantic representation of general topology in the Wolfram Language. In: H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke (eds.) Intelligent Computer Mathematics—10th International Conference, CICM 2017, Edinburgh, UK, July 17–21, Proceedings, Lecture Notes in Computer Science (2017). https://doi.org/10.1007/978-3-319-62075-6_12

23.

Gottliebsen, H., Kelsey, T., Martin, U.: Hidden verification for computational mathematics. J. Symb. Comput. 39(5), 539–567 (2005). https://doi.org/10.1016/j.jsc.2004.12.005MathSciNetCrossRefMATH

24.

Harrison, J.: Formal proofs of hypergeometric sums. J. Autom. Reason. 55(3), 223–243 (2015). https://doi.org/10.1007/s10817-015-9338-0MathSciNetCrossRefMATH

25.

Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and Maple. J. Autom. Reason. 21(3), 279–294 (1998). https://doi.org/10.1023/A:1006023127567

26.

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 ’07 / MKM ’07, pp. 94–105. Springer-Verlag, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_8

27.

Kerber, M., Kohlhase, M., Sorge, V.: Integrating computer algebra into proof planning. J. Autom. Reason. 21(3), 327–355 (1998). https://doi.org/10.1023/A:1006059810729MathSciNetCrossRefMATH

28.

Lewis, R.Y.: An extensible ad hoc interface between Lean and Mathematica. In: C. Dubois, B.W. Paleo (eds.) Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017, EPTCS, vol. 262, pp. 23–37 (2017). https://doi.org/10.4204/EPTCS.262.4

29.

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

30.

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–381. Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3372885.3373824

31.

McBride, C., McKinna, J.: Functional pearl: I am not a number—I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell ’04, pp. 1–9. ACM, New York, NY, USA (2004). https://doi.org/10.1145/1017472.1017477

32.

de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS, pp. 337–340 (2008)

33.

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–388. Springer International Publishing, Cham (2015)CrossRef

34.

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–635. Springer International Publishing, Cham (2021)CrossRef

35.

Pratt, V.R.: Every prime has a succinct certificate. SIAM J. Comput. 4(3), 214–220 (1975)MathSciNetCrossRef

36.

Rabe, F.: The MMT API: a generic MKM system. In: International Conference on Intelligent Computer Mathematics, pp. 339–343. Springer (2013)

37.

Schrijver, A.: Theory of linear and integer programming. Wiley-Interscience Series in Discrete Mathematics. John Wiley & Sons Ltd., Chichester. A Wiley-Interscience Publication (1986)

38.

Seddiki, O., Dunchev, C., Khan-Afshar, S., Tahar, S.: Enabling Symbolic and Numerical Computations in HOL Light, pp. 353–358. Springer International Publishing, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_27

39.

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–182. Springer International Publishing, Cham (2020)CrossRef

40.

Williams, H.: Fourier’s method of linear programming and its dual. The American Mathematical Monthly 93(9), 681–695 (1986)

41.

Wolfram, S.: An Elementary Introduction to the Wolfram Language. Wolfram Media, Incorporated (2015). https://books.google.com/books?id=efIvjgEACAAJ

Title: A Bi-Directional Extensible Interface Between Lean and Mathematica
Authors: Robert Y. Lewis
Minchao Wu
Publication date: 30-01-2022
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 2/2022
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-021-09611-1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner