Given

An experimental project based on a modern and flexible implementation of the E-graph data structure. Unlike most projects focused primarily on compiler optimization, Given is designed for symbolic computation and reasoning. Its goals include:

1. Performing symbolic computations across different mathematical areas.
2. Generating readable mathematical proofs following rules applications.
3. Exploring strategies for integrating modern (and lightweight) LLMs into mathematical reasoning workflows.

Warning

Given is a side project and is not expected to reach a stable state anytime soon.

For more details, contact me.

Getting started

You can either add Given as a local dependency (see Cargo’s documentation on specifying dependencies), or clone the repository and run the examples directly:

# Switch to the latest release
git checkout latest
# Runs the "name" example
cargo run --example name

For now, Given only runs on nightly Rust but should build just fine on stable once some features are stabilized. The standard cargo fmt, clippy and test workflow is available.

Contributions

Contributions are always welcome. However, since the project is still in an exploratory stage and its long-term direction is not yet fully defined, submitted pull requests may not necessarily be merged immediately.

If you are interested in contributing to the ideas explored in Given, consider reaching out first to discuss the proposed changes.