A fully motivated proof is a proof for which the steps are not just correct, but also explainable as the result of a natural search process. Since this concept will very obviously play an essential role in the project, it would be highly desirable to make it precise. So what does it mean for a step of a proof to be "motivated"?
It is perhaps clearer to ask the question negatively. Anyone with a mathematical background will have encountered "rabbits out of hats", that is, steps that appear to come out of nowhere but magically do the job required of them. But what exactly is it about such steps that causes us to view them this way? With a good answer to this question, we could define a motivated proof to be one that contains no rabbits out of hats.
One of the benefits of such a definition would be that it would enable us to set challenge problems of the form "Find a fully motivated proof of S" and have clear rules for what constitutes a solution. One of the reasons for the recent success of the Xena project is that it splits up into a large number of well-defined tasks, for which one can gain undisputed credit. In particular, if you are trying to formalize a given theorem or proof in Lean, then you know that the moment you succeed is precisely the moment that the computer tells you that you have succeeded, so you can have the satisfaction of knowing for certain that you were the first person to formalize a given result, which can be highly motivating. With a formal definition of "fully motivated proof" the hope is that people would derive a similar satisfaction from being the first person to provide a motivated proof of a result that is hard to prove without drawing a rabbit out of a hat.
One potential approach to making precise the notion of what I shall call here a rabbit-free proof is to define a set of "move types" -- that is, methods of transforming a problem -- and defining a motivated proof to be one that can be generated using these move types. The idea is then to design the move types in such a way as to make it impossible to generate rabbits.
This idea does not make much sense without a fuller discussion, but to give an idea of what the distinction between a motivated proof and a regular proof might look like, consider a situation where one wishes to prove an existential statement -- that is, a statement of the form \(\exists x\in X\ P(x)\). A basic rule of logic is that if \(T\) is some term that defines an element of \(X\), then to prove the existential statement it is sufficient to prove the statement \(P(T)\). However, if \(T\) is a fairly complex term, and if the proof that \(P(T)\) holds is quite complicated, then this move can definitely fall into the rabbit-out-of-hat category. So in a motivated proof, we should not expect to allow arbitrary instantiation of an existentially quantified variable.
This might seem to be removing such a fundamental tool that it would make mathematics impossible. However, the word "arbitrary" was important. I do not propose disallowing all instantiation, but instantiation should use terms that are in some sense (to be made precise) generated out of the ingredients served up by the initial statement of the problem. To give a simple example, if we wish to solve the equation \(x^2-46x+525=0\) it is not enough (in a motivated proof) to say "Observe that 21 and 25 satisfy the equation." It is also not enough, though it is slightly better, to say, "Observe that \(x^2-46x+525=(x-23)^2-4\)." But it would be a lot better to say, "We know how to solve quadratic equations of the form $(x+a)^2=b$, so let's see whether we can put our equation into that form. Expanding and rearranging, we find that we would need to choose \(a\) and \(b\) in such a way that \(x^2+2ax+a^2-b=x^2-46x+525\), which tells us that \(a=-23\) and \(b=23^2-525=4\). Thus, our equation is equivalent to the equation \((x-23)^2=4\), which gives \(x=23\pm 2\)."
In the last case, we did not produce any numbers out of nowhere, and we did not produce an algebraic expression out of nowhere that magically happened to equal \((x-23)^2-4\). Even the idea of completing the square did not come out of nowhere, but rather from a natural thought process, that could be summarized as writing down the general form of an equation that we would feel comfortable solving, equating it with the equation we want to solve, obtaining easy equations for the unchosen parameters, and solving those.
That example is given mainly as a useful analogy. The idea is that moves such as instantiating a quantifier should be done only using elements that are generated from the problem itself using "standard moves", just as, for instance, the coefficients in the expression \((x-23)^2-4\) were obtained using some standard algebraic manipulations. But what are these standard moves? Does there even exist a finite set of moves that is sufficient? What should be allowed as a move and what should be forbidden?
Since these all seem to be hard questions and we are unlikely to be able just to write down a satisfactory set of moves without a great deal of thought, it is sensible to break down the task further.
In advance of having a satisfactory formal definition of a motivated proof, it will be helpful to have a number of examples to examine. Each example should consist of a proof for which every step is presented as the outcome of a natural move type. In parallel to this, we should keep a list of move types, described as precisely as possible, that we think we will want to allow. Then the ideal informal motivated proof will be one in which each step is generated by one of the already accepted moves, but it may be that after thinking about how to motivate an argument people will want to propose new move types to add to the list. However, since we do not want the list to grow indefinitely, new move types should be accepted only reluctantly, unless they are very clearly necessary and correspond very clearly to moves that human mathematicians make.
The hope is that this process will lead to a list of move types that is powerful enough to generate a wide range of interesting proofs, but not expressive enough to generate proof steps that human mathematicians would judge as being rabbits out of hats.
The beginnings of a repository of motivated proofs can be found here.