A bi-directional extensible interface between Lean and Mathematica

DOI10.1007/S10817-021-09611-1MaRDI QIDQ2673306zbMATH OpenOpenAlexFDO

Authors Robert Y. Lewis, Minchao Wu

Publication date 9 June 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2101.07758

zbMATH Keywords

computer algebraformalizationproof assistant

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Mathematica®: A Problem-Centered Approach
• Mathematica: a problem-centered approach
• MathemaTB: a \textit{Mathematica} package for tight-binding calculations
• LEAN: An intermediate language based on graph rewriting

Cites work

• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• A formal proof of the irrationality of (3)
• A refinement-based approach to computational algebra in Coq
• A Skeptic's approach to combining HOL and Maple
• Analytica --- an experiment in combining theorem proving and symbolic computation
• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• Dealing with algebraic expressions over a field in Coq using Maple
• Enabling symbolic and numerical computations in HOL Light
• Every Prime Has a Succinct Certificate
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
• Fourier's Method of Linear Programming and Its Dual
• Hammering towards QED
• Hidden verification for computational mathematics
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 1254246 (Why is no real title available?)
• scientific article; zbMATH DE number 1863375 (Why is no real title available?)
• scientific article; zbMATH DE number 1389645 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• scientific article; zbMATH DE number 7699421 (Why is no real title available?)
• Integrating computer algebra into proof planning
• Maintaining a library of formal mathematics
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Semantic representation of general topology in the Wolfram language
• Ten Problems in Experimental Mathematics
• The calculus of constructions
• The Lean 4 theorem prover and programming language
• The Lean theorem prover (system description)
• The Magma algebra system. I: The user language
• The MMT API: a generic MKM system
• Theorema 2.0: computer-assisted natural-style mathematics

Cited in

(3)

• MathemaTB: a \textit{Mathematica} package for tight-binding calculations
• Iscalc: An Interactive Symbolic Computation Framework (System Description)
• Incorporating a database of graphs into a proof assistant

Describes a project that uses

Uses Software

• Coq
• Magma
• Maple
• Mathematica
• Nitpick
• Theorema
• PVS
• z3
• MMT
• QMT
• Analytica
• Lean
• mathlib
• ProofWidgets

This page was built for publication: A bi-directional extensible interface between Lean and Mathematica

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2673306)