egg-bench

January 9, 2026 ยท View on GitHub

PLEASE SUBMIT MORE BENCHMARKS!!!

Theorem proving tasks are allowed, but as it is more unusual, optimization/simplification problems are emphasized.

Benchmarks can just be terms to be optimized in some reasonable machine or human readable presentation. Rules can be links to explicit tables, markdown files of rules, or things in SMTLIB or other existing formats. The goal is to just get things started. Discussions have made it clear that a purely declarative machine readable format is not obviously flexible enough to capture real world needs or the custom programmatic extensions various systems in the literature have implemented.

Table of Contents

  • lambda - problems involving reducing and modelling lambda binders. Untyped Lambda calculus and others
  • polynomial
  • bitvec
  • circuit
  • functional_prog

Links