Juniper - toy Rust CAS with Lean specifications

Stream: general

[Alessandra Simmons]

Not sure if this is the right place to post this, but I wanted to show off this cool little project I made.

Juniper is a toy CAS library built in Rust using Egg, which uses automatically generated rewrite rules from provided Lean theorems. I mostly built it to get familiar with Lean types, Lean metaprogramming, and how Egg works, but I think the overall concept is pretty cool, and I'd definitely like to see CAS projects move in a more formal methods direction.

GitHub repo

[Srivatsa Srinivas]

https://www.youtube.com/watch?v=74VP0SbNHDE

Is a cool talk about how e-graphs are kind of equivalent to using re-write systems in a clever way with a union-find data structure

[Jason Rute]

@Alessandra Simmons Also see the related discussion #general > SOTA on symbolic algebraic systems written in Lean4. You might have some insights to mention there.