Pith. sign in

REVIEW 1 cited by

A bi-directional extensible interface between Lean and Mathematica

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2101.07758 v1 pith:CZMIVTV3 submitted 2021-01-17 cs.LO cs.MS

Robert Y. Lewis , Minchao Wu This is my paper · ORCID
classification cs.LOcs.MS
keywords mathematicaleanproofassistantconnectioninterfaceothersystem
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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. 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A database of constructions of Hadamard matrices

    math.CO 2024-11 conditional novelty 6.0 of 10

    A verified SageMath database now constructs all known Hadamard matrices up to order 1208, corrects the skew Hadamard order 292, updates over 100 table entries, and proves Paley constructions fail for order 2^m times 509203.

Pith tools