When running the tests with the environment variable LODA_TEST_WITH_EXTERNAL_TOOLS=1, the tests will execute the LEAN tool to verify the correctness of the generated formulas. We use LeanFormula::eval() to run the LEAN tool. This should be extended such that it supports creating a temporary LEAN project before evaluating the formula. We want to use this to be able install additional dependencies and use them in the generated LEAN code, e.g.: import Mathlib.Data.Int.Bitwise. The LEAN project should be temporary and only created one in the beginning. It should be possible to initialize and build it using LEAN's lake command.

As a test, we want to support the bitxor function in the LEAN formula generator and map it to the LEAN function Int.xor. This requires import Mathlib.Data.Int.Bitwise. Use the test program A092242 to validate it.