Proof assistants and computer algebra systems have complementary strengths (rigor vs. computational power), but exchanging information between them in a verified way required ad hoc, non-extensible solutions.

The authors implement a user-extensible interface between Lean and Mathematica by reflecting each system's syntax in the other and providing a flexible translation layer. Lean's metaprogramming framework is used to verify Mathematica computations, ensuring the proof assistant's rigor is not compromised.

The interface enables exchange of arbitrary information between Lean and Mathematica. Lean can verify Mathematica's computational results, combining the CAS's power with the proof assistant's trustworthiness, in an extensible architecture users can adapt to new domains.