Papers With

← All papers
First page of A bi-directional extensible interface between Lean and Mathematica

A bi-directional extensible interface between Lean and Mathematica

Robert Y. Lewis, Minchao Wu

cs.LO Jan 17, 2021 · v1
tooling tactic-automation
Read PDF arXiv abstract
TL;DR
Implements a bidirectional interface connecting Lean's proof assistant with Mathematica's computer algebra.
Abstract
The authors implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting each system's syntax in the other and providing flexible translation extensions, they enable the exchange of arbitrary information between the two systems. They demonstrate how Lean's metaprogramming framework can verify certain Mathematica computations so that the rigor of the proof assistant is not compromised, while Mathematica serves as an untrusted oracle to guide proof search in Lean.
Problem

Lean and Mathematica have complementary strengths (rigorous verification vs. powerful computation), but no extensible interface existed to exchange arbitrary information between the two systems while maintaining proof-assistant rigor.

Approach

The authors implement a bi-directional, user-extensible ad hoc connection between Lean and Mathematica by reflecting each system's syntax in the other and providing flexible translation extensions. Lean's metaprogramming framework verifies certain Mathematica computations so that proof-assistant rigor is not compromised, while Mathematica serves as an untrusted oracle to guide proof search.

Results

The interface enables exchange of arbitrary information between Lean and Mathematica, allowing Mathematica computations to guide Lean proof search without compromising the trusted kernel. The extensible design lets users add new translations for their specific domains.