A bi-directional extensible interface between Lean and Mathematica
From MaRDI portal
Publication:2673306
DOI10.1007/s10817-021-09611-1OpenAlexW3122538476MaRDI QIDQ2673306
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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
- The calculus of constructions
- A Skeptic's approach to combining HOL and Maple
- Analytica --- an experiment in combining theorem proving and symbolic computation
- Integrating computer algebra into proof planning
- The Magma algebra system. I: The user language
- The Lean 4 theorem prover and programming language
- Maintaining a library of formal mathematics
- Semantic representation of general topology in the Wolfram language
- Hidden verification for computational mathematics
- Dealing with algebraic expressions over a field in Coq using Maple
- The MMT API: A Generic MKM System
- A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
- A Refinement-Based Approach to Computational Algebra in Coq
- Ten Problems in Experimental Mathematics
- Enabling Symbolic and Numerical Computations in HOL Light
- The Lean Theorem Prover (System Description)
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Fourier's Method of Linear Programming and Its Dual
- Every Prime Has a Succinct Certificate
- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
- Hammering towards QED
- Theorema 2.0: Computer-Assisted Natural-Style Mathematics
- Certified Computer Algebra on Top of an Interactive Theorem Prover
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
This page was built for publication: A bi-directional extensible interface between Lean and Mathematica
