An Extensible Ad Hoc Interface between Lean and Mathematica
Robert Y. Lewis (Carnegie Mellon University)
TL;DR
This paper presents a flexible, extensible interface enabling seamless communication and verification between the Lean proof assistant and Mathematica, enhancing their interoperability while maintaining proof rigor.
Contribution
It introduces a novel user-extensible connection that reflects syntax and allows for verified computations, bridging formal proof and symbolic computation systems.
Findings
Implemented a reflective, extensible interface between Lean and Mathematica
Verified Mathematica computations within Lean to ensure proof rigor
Facilitated exchange of arbitrary information between the two systems
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.