One of the central theoretical aims of the project is to come up with a finite set of move types that can be used to generate all proofs that a human would judge to be "motivated", in the sense that they do not involve drawing a rabbit out of a hat. (For basic definitions we use, such as that of a "move type", see this post.) This problem splits naturally into two subproblems: say more precisely what counts as a "rabbit out of a hat", and devise the set of move types.
One clear example of a step that should count as a rabbit out of a hat is instantiation of a quantifier with a term that is not in any sense "present" in the current problem state. So we can insist that all instantiations must be with variables or more complex terms that have already been generated using moves from the small set of move types. (It is also important to place restrictions on what is allowed as a move type. For example, if we want to ban producing an arbitrary formula out of nowhere, we must make sure that our moves are not expressive enough to encode arbitrary formulae.)
A move type that is fundamental to doing mathematics is that of combining a hypothesis one has generated with a result one already knows in order to deduce a further piece of information. For instance, if one has established that a set $A$ is a compact subset of a topological space $X$ and that $f:X\to Y$ is a continuous function, one might want to deduce that $f(A)$ is a compact subset of $Y$. This raises the following question.
Question. Under what circumstances should the use of a library result be classed as motivated?
It seems clear that there will have to be some restriction, since if every library reasoning step is permitted in a motivated proof, that would appear to make it possible to generate any proof, whether or not we would judge it to involve a miraculous idea.
To clarify the discussion a little bit, let us consider two different kinds of "miracles" that we would like to avoid.
I'm not sure how important the distinction between the above two forms of "lack of motivation" is. In one case we extract an apparently irrelevant result from the library, which, once we decide we are going to use it, provides us with plenty of motivation for the steps that follow -- we know we want to create some dense open sets, and so on. In the other case, we do a series of library modus ponens steps, and what makes it unmotivated is that there are many deductions we could have made from our hypotheses using library results, and no clear reason for choosing the ones we chose.
Now let's think what a motivated use of the Baire category theorem might look like. This is closely related to the question of how an experienced human mathematician might notice that the theorem can be applied. We might find, for instance, that we want to prove a statement of the form $\exists x\in X\ \forall n\in\mathbb N\ P(n,x)$, where $X$ is a metric space. We might observe that the weaker statement where the quantifiers are reversed, namely $\forall n\in\mathbb N\ \exists x\in X\ P(n,x)$, is quite easy to prove, in which case we would say to ourselves "It's fine if $x$ is allowed to depend on $n$, but I want it to hold uniformly." And then our experience would tell us that there are tools around that allow us, under suitable circumstances, to obtain uniform statements: roughly speaking we need each $P(n,x)$ to hold not just for some $x$ but for almost all $x$, where there are several possible interpretations of "almost all" that can be useful. Here we are discussing the category notion of "almost all" but another is the measure-theoretic notion, where the set of $x$ that do not satisfy $P(n,x)$ has measure zero. We might then look at the problem and see that there is no obvious measure about, but that it is definitely worth checking whether $\{x:P(n,x)\}$ is dense and open. We might even take note of encouraging hints of this, such as that the property $P(n,x)$ involves strict inequalities rather than non-strict ones.
There's quite a lot going on here, and much of it looks as though it might be quite hard to model. For instance, the explanation above relied on a somewhat vague and abstract notion of "suitable 'almost all' definition". However, while imprecise language often plays a role in the process by which human mathematicians discover proofs, it is not clear how essential it is for this kind of search. Maybe one could make it precise by defining a formal notion of "a system of small subsets of $X$", which would obey axioms such as "A countable union of small sets is small" and "$X$ is not small". Then we could have a very general library result that said that the statement $\exists x\in X\ \forall n\in\mathbb N\ P(n,x)$ is true if there is a system $\Sigma$ of small sets such that for every $n$ the set $\{x\in X:\neg P(n,x)\}$ is small. And finally there would be some library results to say that the nowhere dense sets in a metric space are a system of small sets, as are the sets of measure zero in $\mathbb R$. These results would not be what we normally think of as theorems. Rather, they would be formal statements of heuristic principles, and the purpose of having them in the library would be to model the know-how of an experienced human mathematician, providing a bridge between a problem state where a library result can be applied in a non-obvious way, and the library result itself.
A slight worry here is that we don't want to cheat by simply adding motivating principles to the library every time we can't see how to find a motivation for extracting a library result. But I'm not too worried by that. If an undergraduate asked the question "How on earth did you think of using the Baire category theorem?" and received an explanation along the lines given above (about needing to have a suitable notion of "almost all" in order to obtain uniformity), then I think they would find it convincing. And if a human mathematician does not have a heuristic principle such as the above one in their personal library (that is, the bank of knowledge they carry around in their brain) then they will normally be quite bad at spotting that the Baire category theorem can be used.
I do not have a complete answer -- hence the word "towards" -- but let me try to find conditions that seem to be necessary and conditions that seem to be sufficient (but not necessarily a set of conditions that between them are necessary and sufficient).
I thought I was going to have more to say there, but actually I don't. I'm wondering whether the first condition might in fact be necessary and sufficient, at least when appropriately formulated.
To test that thought, let me try to think about the Baire category theorem example once more. If we had the statement $\exists x\in X\ \forall n\in\mathbb N\ P(n,x)$ as a target, the proposal above was that we would use library reasoning to convert that into a statement that would say something along the lines of "There is a notion of smallness such that for each $n$ the set of $x$ such that $\neg P(n,x)$ is small." But what intermediate goal would be achieved by reformulating the target in this way?
As a human mathematician I might say something like this. "Typically, proving uniform statements is hard, and one needs suitable tools to do it. There aren't very many standard tools of this kind, so let's see if we can find one that works." But somehow that doesn't easily translate into the language of problem states and their features. That is, what would make the target $$ \exists\Sigma\ \forall n\in\mathbb N\ \text{small}_\Sigma( \{ x\in X:P(n,x) \} ) $$ preferable to the target $$\exists x\in X\ \forall n\in\mathbb N\ P(n,x)?$$
A possible answer comes if we invent a new notation, writing $(\Lambda_\Sigma\ x)\ Q(x)$ to mean $\{x:\neg Q(x)\}\in\Sigma$. This would be read as "for almost all (in the sense of $\Sigma$) $x$, $Q(x)$". In this notation the first target would now read $$\exists\Sigma\ \forall n\in\mathbb N\ (\Lambda_\Sigma\ x)\ P(n,x).$$ This would be better than the first target because the quantifiers would have been reversed (at the cost of replacing "there exists" by the much stronger "for almost all (in the sense of $\Sigma$)".
But that still feels unsatisfactory, because the improvement is not a syntactic feature of the problem state, but rather a mathematical one -- we somehow know from experience that replacing a uniform statement by a non-uniform one has a good chance of being helpful. Maybe that idea can itself be encoded as a formal statement in the library, though I'm not sure I see how to do it.
There's another thought I have had at various moments that I think might help here. I've already suggested that motivated library reasoning should come as the result of searching with some goal in mind. Perhaps one way of generating a goal is to allow an abstraction move, the idea of which would be to modify the target by abstracting and generalizing it. In that way, rather general library results that previously would not have directly matched the target would now do so, and if there were not too many of them, then this search process might count as a motivation.
I would see this process working as follows. If one fails to find a move that achieves a subtask, then one raises the level of abstraction and attempts, at the more abstract level, to find a move that achieves a subtask, possibly continuing that process for several steps. When enough has been abstracted away from the original problem state, the options will become more limited, and what it will achieve is to suggest not a proof step but a proof strategy. It could be thought of as a way of including something like general proof plans in the library and searching for them.
A possible answer to the question of what constitutes a motivated library extraction is that it is the use of a library result that has been obtained as the result of a search, where the search itself has been conducted using standard proof-finding methods such as trying to find matches for terms. With the Baire category theorem example above, it is quite hard to analyse its use in that way, but a potential way of making it easier is to allow abstraction as one of the proof-finding methods (which I certainly think it should be anyway), which allows the proof finder to search for general techniques for proving a wide class of statements, as opposed to results that are more tailored to the specific target and hypotheses in the given problem state.
Thus, part of what we would need to do in order to design a motivated-proof finder is fix what the allowable methods are for searching the library. As usual, I think it is very useful to imagine a system where direct typing in of text is banned. Instead, everything would be done with highlighting text and selecting options from small menus. For instance, one might select "forwards library reasoning" from a "move type" menu, and then be prompted with "using which hypothesis?", and then with "motivation?" where to that last question one might select "create match for term ..." and then highlight the desired term and hit carriage return. At that point the system would search for a library result that did the job. If it didn't find one, one would have to try something else. If it found a vast number of possibilities, then maybe there could be an "add motivation?" option to try to narrow them down. If there was just one possibility that would of course be easy. That leaves the interesting case of what happens when there is more than one possibility but a manageable number such as two or three.
I think that situation is quite interesting. One possibility would be to display the possibilities to the user and let the user make a choice. But that in principle allows the user to make a choice based on significant mathematical knowledge that is hidden from the program, and looks as though it could allow rabbits to sneak in. So instead I would suggest that the program does not reveal what the library results are but merely numbers them randomly. Or perhaps it could inform the user if using one of the results leads to desirable features that had not been asked for (such as creating a match for another term as well). Then the user who did not single out a unique library result would be forced to do some kind of search, which might reflect quite well the sort of search we really do do when looking for proofs. (A small complication here is that some results might have lots of variants and minor reformulations. I think the library would need to be aware of this, so that if say ten results achieve a given objective and nine of them are equivalent, then the program treats the situation as though there were two options rather than ten.)
I also think we should be open to anxiety measures here. For example, we might decide that use of the Baire category theorem is a sensible thing to try, but not have a clear idea of whether the sets in question are going to turn out to be open and dense, which will make us a little anxious. But once we formulate subtargets such as $\text{is_dense}(\{x:P(n,x)\})$, we may find that lots of motivated moves are possible, which will greatly reduce that anxiety.
What I'm saying here is that we may find that motivating every single move before it happens is just unrealistic, and that we'll have to allow a small amount of search -- if there are very few branches and one of the branches, though not in itself obviously motivated, leads after one further motivated step to some highly desirable features, then it would be in some sense "confirmed" as a good branch.