One goal for a powerful automated prover is to be able to add results it has discovered to the library. But when a result is discovered, how do we know if it is a good idea to add it to the library? It might be tempting to always add to the library, but that has the potential of cluttering up the library with useless junk. I propose a criterion which is based on minimising a quantity I will refer to as the entropy.
Suppose we have a family $\mathcal{F}$ of proofs we have found, and our current library is $L$. By abstraction we might have identified a result $r$ that we could add to the library. In order to decide whether to add $r$ to the library, we use a criterion inspired by the DreamCoder paper. We construct the library in such a way as to minimise the entropy
$$ S := c_LS(L) + \sum_{f \in \mathcal{F}} S(f). $$
Here we are not overly specific about what exactly the entropy is. For proofs, a vague definition would be the amount of choice we have to make in order to discover the proof. This is basically a measure for how hard the proof is to find. In particular, if the proof discovery process involves a library search which has $n$ results and we pick one of these results, then this contributes $\log n$ to the entropy. The constant $c_L$ determines how much we care about the simplicity of our library. It is not unreasonable to set $c_L = 0$ as library searchability already imposes restrictions to the library.
If we were to add $r$ to the library, the entropy would change by an amount
$$ \Delta S = c_L(S(L \cup \{ r \}) - S(L)) + \sum_{\lambda \in \mathrm{LS1}} \log \left( 1 + \frac{1}{|\mathrm{results}(\lambda)| - 1}\right) $$ $$ + \sum_{\lambda \in \mathrm{LS2}} \left(\log(|\mathrm{results}(\lambda)|) - S(\mathrm{replaced\;proof}(\lambda))\right) $$
and so we should add the new result to the library if the above quantity is negative. In the above, $\mathrm{LS1}$ refers to the set of library searches for proofs in $\mathcal{F}$ where $r$ would be an option and we don't pick $r$, while $\mathrm{LS2}$ refers to the set of library searches where $r$ is an option and we do pick $r$. The function "results" just returns the number of results of the relevant library search, while "replaced proof" refers to the portion of the proof discovery process we no longer have to do when we use the new result $r$ returned by the relevant library search. Typically $S(\mathrm{replaced \ proof}(\lambda))$ can be approximated by $S(r)$, the entropy required to prove $r$ as a free standing result.
The basic idea is that if the result saves us a lot of work $S(\mathrm{replaced \ proof}(\lambda))$, then it is good to have it in the library, whereas if the result would be hard to find $\log(|\mathrm{results}(\lambda)|)$ or it clutters up the search too much $\log(1 + 1/(|\mathrm{results}(\lambda)|-1))$ then that discourages us.