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.
| Original language | English |
|---|---|
| Pages (from-to) | 215-238 |
| Number of pages | 24 |
| Journal | Journal of Automated Reasoning |
| Volume | 66 |
| Issue number | 2 |
| Early online date | 30 Jan 2022 |
| DOIs | |
| Publication status | Published - May 2022 |
Bibliographical note
Funding Information:We acknowledge Jeremy Avigad, Jasmin Blanchette, Ian Ford, Johannes H?lzl, Jos? Mart?n-Garc?a, Leonardo de Moura, James Mulnix, Michael Trott, and the Lean community for help, suggestions, and support.
Funding Information:
The first author receives support from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka) and from the Dutch Research Council (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward)
Publisher Copyright:
© 2021, The Author(s), under exclusive licence to Springer Nature B.V.
Keywords
- Computer algebra
- Formalization
- Proof assistant