A Bi-Directional Extensible Interface Between Lean and Mathematica

Robert Y. Lewis*, Minchao Wu

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


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 languageEnglish
Pages (from-to)215-238
Number of pages24
JournalJournal of Automated Reasoning
Issue number2
Early online date30 Jan 2022
Publication statusPublished - 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.


  • Computer algebra
  • Formalization
  • Proof assistant


Dive into the research topics of 'A Bi-Directional Extensible Interface Between Lean and Mathematica'. Together they form a unique fingerprint.

Cite this