nach oben

Tipp

A Bi-Directional Extensible Interface Between Lean and Mathematica

verfasst von: Robert Y. Lewis, Minchao Wu

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2022

Einloggen, um Zugang zu erhalten

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.

Vorheriger Artikel A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Nächster Artikel Analyzing Read-Once Cutting Plane Proofs in Horn Systems

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

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:1006079212546 MathSciNetCrossRefMATH

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.0125 MathSciNetCrossRefMATH

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/4568 MathSciNetCrossRefMATH

13.

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

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-3 MathSciNetCrossRefMATH

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.004 MathSciNetCrossRefMATH

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.005 MathSciNetCrossRefMATH

24.

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

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:1006059810729 MathSciNetCrossRefMATH

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

Titel: A Bi-Directional Extensible Interface Between Lean and Mathematica
verfasst von: Robert Y. Lewis
Minchao Wu
Publikationsdatum: 30.01.2022
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 2/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-021-09611-1

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

A Bi-Directional Extensible Interface Between Lean and Mathematica

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner