We have been running experiments to evaluate various strategies for automating the discovery of abstractions with the goal of assisting twee (an automated equational theorem prover, see linked webpage) in discovering shorter or unknown proofs of abstract algebraic theorems. The previous project storage is ending, and we need a new storage allocation to keep the existing and future experiment logs.
Preliminary results were reported at the 10th Conference on Artificial Intelligence and Theorem Proving (AITP 2025, slides available at https://aitp-conference.org/2025/). All compute for these experiments was done on the e-infrastructure compute allocation for CSE vera project.