OSCAR relies on many software packages. For a complete and up-to-date list of dependencies, please see the Project.toml file in the OSCAR GitHub repository. The following are some of them:
The Mathematical Research Data Initiative (MaRDI), is a German consortium dedicated to setting guidelines and developing software for findability, accessibility, interoperability, and reuse of mathematical research data. OSCAR’s serialization employs the mrdi file format, the specifications of which can be found on zenodo. More details are available in this article and the OSCAR documentation.
The LEAN proof assistant is a formal system for writing and verifying mathematical proofs using a computer. While OSCAR is designed to perform concrete symbolic computations in areas such as algebra and geometry, LEAN is tailored for the formalization and verification of abstract mathematical reasoning.
An initial connection between these two systems has been explored in the meeting LEAN meets MaRDI and OSCAR (Berlin, December 2024) and most notably in the Lean-Oscar repository, originally created by Cedric Holle. This proof-of-principle demonstrates how OSCAR can support formal proofs in LEAN. Such an interaction opens up promising avenues for collaboration and research, allowing mathematicians to bridge the gap between rigorous computation and rigorous proof.
