An Extensible Ad Hoc Interface between Lean and Mathematica

Robert Y. Lewis
(Carnegie Mellon University)

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.

In Catherine Dubois and Bruno Woltzenlogel Paleo: Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving (PxTP 2017), Brasília, Brazil, 23-24 September 2017, Electronic Proceedings in Theoretical Computer Science 262, pp. 23–37.
Published: 4th December 2017.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: