A work-in-progress Lean 4 binding to GiNaC, which is an open-source symbolic computation library in C++, it has extensive algebraic capabilities, and has been specifically developed to be an engine for high energy physics applications.
See this doc to learn more.
The work started on Sep 18, 2023, and it's still at an early stage, mostly a POC, and nowhere near a complete binding. It's encouraged to draw inspiration from this project, but it's not recommended to use it in production.
This project is still on my thoughts, and I'm still trying to figure out the best way to proceed.
If one is interested in using GiNaC in Lean, discussions are welcome (by opening an issue, or pinging me on Lean Zulip), including about creating other bindings.
lake -R build
# Follow https://pre-commit.com/ to install pre-commit
# pyenv shell 3.11
# brew install pre-commit
# pre-commit installTL;DR: Practically, if one uses GinacLean to use GiNaC, one must comply with the GPL license. But this repository itself only contains MIT licensed code.
GinacLean itself is licensed under the MIT license, see LICENSE for details. It means any code at rest in this repository can be considered as MIT licensed.
But GiNaC is licensed under the GPL license (version 2 or later), see COPYING for details. When built or at runtime, GinacLean interacts with the GPL licensed GiNaC library, thus the GPL license applies to all of GinacLean. See this answer on SE for more details.
GiNaC depends on CLN which is also GPL licensed. The discussion above applies to CLN as well.
One subtlety is that in releases of GinacLean, GiNaC/CLN might be included (thus redistributed), so any such release should be considered as GPL licensed. But the plan is to make no such releases.