# A family of diophantine equations of the form
$x^{4}+2nx^{2}y^{2}+my^{4}=z^{2}$ with no solutions in
$({\mathbb{Z}}^{+})^{3}$

Konstantine Zelator
Department of Mathematics
College of Arts and Sciences
Mail Stop 942
The University of Toledo
Toledo, OH 43606-3390
e-mails<EMAIL_ADDRESS>
<EMAIL_ADDRESS>
##  1 Introduction

In this work we present a family of diophantine equations of the form

$x^{4}+2nx^{2}y^{2}+my^{4}=z^{2}$ (1)

with no nontrivial solutions.

This is done in Section 3, where the theorem in this paper, Theorem 1, and its
proof are presented. The approach is elementary and uses only congruence
arguments as well as decent. It is branched proof, with some of the branches
leading to contradictions via congruence arguments. Two of the proof’s
branches lead to contradictions via a decent argument. Also in the proof, we
make use of the well-known parametric formulas that describe all the solutions
in $({\mathbb{Z}}^{+})^{3}$ to the diophantine equation $x^{2}+\ell\cdot
y^{2}=z^{2}$, $\ell$ a positive integer. These formulas are found in Section
2. In Section 4, we present a sampling of numerical examples. That is, a
listing of combinations of integers $n$ and $m$ in (1), which satisfy the
hypothesis of the theorem.

The paper concludes with Section 5, wherein we offer a brief historical
commentary on diophantine equations of the form
$ax^{4}+bx^{2}y^{2}+cy^{4}=dz^{2}$. Investigations of these types of
diophantine equations span a time interval of nearly 400 years, not to go back
any further in time. We mention some of the results found in the literature,
including more recent developments (of the last 70 years) on the subject
involving the usage of local methods as well as the association of such
equations with elliptic curves.

##  2 An auxiliary diophantine equation:
$x^{2}+\ell\cdot y^{2}=z^{2}$

For a given positive integer $\ell$, the solution set (subset of
$({\mathbb{Z}}^{+})^{3}$) of the diophantine equation $x^{2}+\ell
y^{2}=z^{2}$, can be parametrically described by the formulas,

$x=\dfrac{d(\rho_{1}k^{2}-\rho_{2}\lambda^{2})}{2},\ y=dk\lambda,\ \
z=\dfrac{d(\rho_{1}k^{2}+\rho_{2}\lambda^{2})}{2}$

where the parameters $d,k,\lambda$ are positive integers such that
$(k,\lambda)=1$; and the positive integers $\rho_{1},\rho_{2}$ are divisors of
$\ell$ such that $\rho_{1}\rho_{2}=\ell$. Obviously, if we require that
$(x,y)=1$, then all the solutions in $({\mathbb{Z}}^{+})^{3}$ can be
parametrically described as follows:

$\left\\{\begin{array}[]{l}x=\dfrac{d(\rho_{1}k^{2}-\rho_{2}\lambda^{2})}{2},\
y=dk\lambda,\ \ z=\dfrac{d(\rho_{1}k^{2}+\rho_{2}\lambda^{2})}{2},\\\ \\\ {\rm
with}\ d,k,\lambda,\rho_{1},\rho_{2}\in{\mathbb{Z}}^{+}\ {\rm such\ that}\
(k,\lambda)=1,\ \rho_{1}\rho_{2}=\ell\\\ \\\ {\rm and\ with}\ d=1\ {\rm or}\
2.\ {\rm Also},\ \rho_{1}k^{2}-\rho_{2}\lambda^{2}>0.\end{array}\right\\}$ (2)

These parametric formulas are well known in the literature and can be found in
reference [1], (pages 420-421). A derivation of them can also be found in [2].

##  3 The theorem and its proof

Theorem 1: Suppose that $n$ is a positive integer, $p$ an odd prime, and such
that either

$\begin{array}[]{lcll}n\equiv 0\ ({\rm mod}\ 4)&{\rm and}&p\equiv 3\ ({\rm
mod}\ 8);&{\rm or\ alternatively},\\\ \\\ n\equiv 2\ ({\rm mod}\ 4)&{\rm
and}&p\equiv 7\ ({\rm mod}\ 8)\end{array}$

In addition to the above, assume that one of the following hypotheses holds:

either

  1. (i)

$n^{2}-p>0$ and the positive integer $m=n^{2}-p$ is a prime, or

  2. (ii)

$n^{2}-p<0$ and the positive integer $N=-m=-(n^{2}-p)$ is a prime.

Then, the diophantine equation $x^{4}+2nx^{2}y^{2}+my^{4}=z^{2}$ has no
solution in $({\mathbb{Z}}^{+})^{3}$.

Proof: If equation (1) has a solution, then let $(X_{0},Y_{0},Z_{0})$ be a
solution with the product $X_{0}Y_{0}$ being least. Let
$\delta=(X_{0},Y_{0})$, so that $X_{0}=\delta x_{0},\ Y_{0}=\delta y_{0}$, for
positive integers $x_{o},y_{0},\delta$ such that $(x_{0},y_{0})=1$. Then, (1)
implies $\delta^{4}\mid Z^{2}_{0}$ and so $\delta^{2}\mid Z_{0}$; and by
putting $Z_{0}=\delta z_{0}$ for some $z_{0}\in{\mathbb{Z}}^{+}$ we obtain

$x^{4}_{0}+2nx^{2}_{0}y^{2}_{0}+my^{4}_{0}=z^{2}_{0}$ (3)

By (3), the triple $(x_{0},y_{0},z_{0})$ is a solution to equation (1). Thus,
by the minimality of the product $X_{0}Y_{0}$ it follows that $\delta=1,\
X_{0}=x_{0},\ Y_{0}=y_{0},\ Z_{0}=z_{0}$.

Since $x_{0}$ and $y_{0}$ are relatively prime, there are three possibilities:

$x_{0}\equiv y_{0}\equiv 1\ ({\rm mod}\ 2);\ x_{0}\equiv 0\ {\rm and}\
y_{0}\equiv 1\ ({\rm mod}\ 2);\ {\rm or}\ x_{0}\equiv 1\ {\rm and}\
y_{0}\equiv 0\ ({\rm mod}\ 2).$

If $x_{0}$ and $y_{0}$ are both odd, consider equation (3) modulo 4. Since
$x^{2}_{0}\equiv y^{2}_{0}\equiv 1\ ({\rm mod}\ 4)$, in this case, (3) implies
$1+2n+m=z^{2}_{0}\ ({\rm mod}\ 4)$. By the Theorem’s hypothesis, $2n\equiv 0\
({\rm mod}\ 4)$ and $m=n^{2}-p$; we obtain $1-p\equiv z^{2}_{0}\ ({\rm mod}\
4)$, which gives $z^{2}_{0}\equiv 2\ ({\rm mod}\ 4)$ in view of $p\equiv 3\
({\rm mod}\ 4)$, an impossibility.

Next consider the second possibility. The combination $x_{0}$ being even and
$y_{0}$ odd. By (3), since $m$ is odd, we see that $z_{0}$ must be odd as
well. Consider (3) modulo 8. In view of $y^{2}_{0}\equiv z^{2}_{0}\equiv 1\
({\rm mod}\ 8)$, (3) implies $m\equiv 1\ ({\rm mod}\ 8)$, a contradiction
since by hypothesis:

$m=n^{2}-p\equiv 0-3\equiv 5\ ({\rm mod}\ 8),\ {\rm if}\ n\equiv 0\ ({\rm
mod}\ 4)\ {\rm and}\ p\equiv 3\ ({\rm mod}\ 8),$

while also,

$m=n^{2}-p\equiv 4-7\equiv 5\ ({\rm mod}\ 8),\ {\rm if}\ n\equiv 2\ ({\rm
mod}\ 4)\ {\rm and}\ p\equiv 7\ ({\rm mod}\ 8).$

We conclude that $x_{0}$ must be odd and $y_{0}$ even. Also, it is clear from
(3) that since $(x_{0},y_{0})=1$, $y_{0}$ and $z_{0}$ must be relatively prime
as well; and $z_{0}$ must be odd. Therefore,

$\left\\{\begin{array}[]{l}x^{4}_{0}+2nx^{2}_{0}y^{2}_{0}+my^{4}_{0}=z^{2}_{0}\\\
\\\ x_{0}\equiv z_{0}\equiv 1\ ({\rm mod}\ 2),\ y_{0}\equiv 0\ ({\rm mod}\
2)\\\ \\\ (x_{0},y_{0})=1=(y_{0},z_{0})\end{array}\right\\}$ (4)

Now we use the hypothesis that $m=n^{2}-p$. An algebraic manipulation of the
equation in (4) leads to,

$\begin{array}[]{rcl}(x^{2}_{0}+ny^{2}_{0})^{2}-z^{2}_{0}&=&py^{4}_{0};\\\ \\\
\left[(x^{2}_{0}+ny^{2}_{0})+z_{0}\right]\left[(x^{2}_{0}+ny^{2}_{0})-z_{0}\right]&=&py^{4}_{0}\end{array}$
(5)

According to the conditions in (4) both $(x^{2}_{0}+ny^{2}_{0})$ and $z_{0}$
are odd integers, but they are also coprime. Indeed, if a prime $q\neq p$ were
a common divisor of theirs, then by (5) it would also divide $y_{0}$ and
therefore, $x_{0}$ as well, violating $(x_{0},y_{0})=1$. If $p$ divided both
$(x^{2}_{0}+ny^{2}_{0})$ and $z_{0}$, then $p^{2}$ would divide the left-hand
side of (5), and thus $p$ would divide $y_{0}$. Hence, it would divide
$x_{0}$, contrary once more to $(x_{0},y_{0})=1$. We conclude that

$(x^{2}_{0}+ny^{2}_{0},z_{0})=1$ (6)

Moreover, the sum of any two odd integers is congruent to $0\ ({\rm mod}\ 4)$
and their difference to $2\ ({\rm mod}\ 4)$; or vice-versa. Combining this
observation with (6) leads to,

$\left\\{\begin{array}[]{l}x^{2}_{0}+ny^{2}_{0}+z_{0}=2\delta_{1}\\\ \\\
x^{2}_{0}+ny^{2}_{0}-z_{0}=2\delta_{2}\\\ \\\ {\rm for}\
\delta_{1},\delta_{2}\in{\mathbb{Z}}^{+},\ {\rm with}\
(\delta_{1},\delta_{2})=1\ {\rm and}\ \delta_{1}+\delta_{2}\equiv 1\ ({\rm
mod}\ 2)\end{array}\right\\}.$ (7)

Adding the two equations in (7) yields,

$x^{2}_{0}+ny^{2}_{0}=\delta_{1}+\delta_{2}.$ (8)

According to (7), $\delta_{1}$ must be even and $\delta_{2}$ odd; or vice-
versa. Given that the rest of the proof rests on (8) and that (8) is symmetric
in $\delta_{1}$ and $\delta_{2}$. There is no need to distinguish between two
cases, they lead to the same contradictions. Accordingly, assume that
$\delta_{1}$ is even and $\delta_{2}$ is odd.

If we combine (7) with (5), we see that since $p$ is an odd prime, there are
precisely two possibilities expressed in (9) below:

$\begin{array}[]{lllll}{\rm Either}&2\delta_{1}=8py^{4}_{1}&{\rm
and}&2\delta_{2}=2y^{4}_{2}&\hskip 72.26999pt{\rm(9a)}\\\ {\rm
or}&2\delta_{1}=8y^{4}_{1}&{\rm and}&2\delta_{2}=2py^{4}_{2}&\hskip
72.26999pt{\rm(9b)}\end{array}$
for positive integers $y_{1},y_{2},$ such that $(y_{1},y_{2})=1$
and $y_{2}\equiv 1\ ({\rm mod}\ 2)$.
Note that in either case, we have from (5), $2y_{1}y_{2}=y_{0}$. (9)

Case 1: Assume possibility (9b) in (9) to hold. Then by combining (9b) with
(8) gives

$x^{2}_{0}+ny^{2}_{0}=4y^{4}_{1}+py^{2}_{2},$

which is impossible modulo 4, since by (4) we have $x^{2}_{0}+ny^{2}_{0}\equiv
1\ ({\rm mod}\ 4)$, while $4y^{4}_{1}+py^{4}_{2}\equiv p\equiv 3\ ({\rm mod}\
4)$, in view of the hypothesis of the theorem.

Case 2: Assume possibility (9a) to be the case in (9).

Subcase 2(i): Assume hypothesis (i) in the theorem, which means that the
integer $n^{2}-p=m$ is positive and a prime. By combining (9a) with (8) and
$2y_{1}y_{2}=y_{0}$ in (9) we obtain

$x^{2}_{0}+(n^{2}-p)\cdot(2y^{2}_{1})^{2}=(y^{2}_{2}-2ny^{2}_{1})^{2}$ (10)

According to (10), the triple
$(x_{0},2y^{2}_{1},\left|y^{2}_{2}-2ny^{2}_{1}\right|)$ is a positive integer
solution to the diophantine equation $x^{2}+\ell y^{2}=z^{2}$, with
$\ell=n^{2}-p$. Also note that $(x_{0},2y^{2}_{1})=1$, by virtue of the fact
that $(x_{0},y_{0})=1$ in (4) and $y_{0}=2y_{1}y_{2}$ in (9). Therefore, by
(2), we must have

$\left\\{\begin{array}[]{l}2y^{2}_{1}=dk\lambda,\
\left|y^{2}_{2}-2ny^{2}_{1}\right|=\dfrac{d(\rho_{1}k^{2}+\rho_{2}\lambda^{2})}{2},\
{\rm for\ positive}\\\ {\rm integers}\ d,k,\lambda,\rho_{1},\rho_{2};\ {\rm
such\ that}\ (k,\lambda)=1,\ \rho_{1}\rho_{2}=n^{2}-p\\\ {\rm and\ with}\ d=1\
{\rm or}\ 2\end{array}\right\\}$

(10a)

The possibility $d=1$ is easily ruled out by the fact that $\rho_{1}$ and
$\rho_{2}$ are both odd (since $m=n^{2}-p$ is odd); and the fact that
$(k,\lambda)=1$. Indeed, the first equation (10a) implies, if $d=1$, that $k$
and $\lambda$ must have different parities. But, then the integer
$\rho_{1}k^{2}+\rho_{2}\lambda^{2}$ would be odd, instead of even as the
second equation in (10a) requires. Thus, $d=2$ which yields, by (10a)

$\begin{array}[]{l}y^{2}_{1}=k\lambda,\
\left|y^{2}_{2}-2ny^{2}_{1}\right|=\rho_{1}k^{2}+\rho_{2}\lambda^{2};\ {\rm
or\ equivalently}\\\ \\\ \left\\{y^{2}_{1}=k\lambda,\
y^{2}_{2}-2ny^{2}_{1}=\pm(\rho_{1}k^{2}+\rho_{2}\lambda^{2})\right\\}\end{array}$

(10b)

The first equation in (10b) implies, since $(k,\lambda)=1$, that $k=k^{2}_{1}\
{\rm and}\ \lambda=\lambda^{2}_{1};\ {\rm for\ some}\
\lambda_{1},k_{1}\in{\mathbb{Z}}^{+},\ {\rm with}\ (k_{1},\lambda_{1})=1.$

Accordingly (10b) gives,

$y^{2}_{2}-2nk^{2}_{1}\lambda^{2}_{1}=\pm(\rho_{1}k^{4}_{1}+\rho_{2}\lambda^{4})$
(10c)

since $y_{1}=k_{1}\lambda_{1}$.

If the plus sign holds in (10c), we obtain

$y^{2}_{2}=\rho_{1}k^{4}_{1}+2nk^{2}_{1}\lambda^{2}_{1}+\rho_{2}\lambda^{4}_{1}$
(10d)

By (10a) we know that $\rho_{1}\rho_{2}=m=n^{2}-p$. But $m$ is a prime and so
either $\rho_{1}=m$ and $\rho_{2}=1$ or vice-versa. In either case, (10d)
shows that the triple $(k_{1},\lambda_{1},y_{2})$ is a positive integer
solution to the diophantine equation (1). Compare this solution with the
solution $(x_{0},y_{0},z_{0})$ (see (3)). We have

$x_{0}y_{0}\geq y_{0}=2y_{1}y_{2}>y_{1}=k_{1}\lambda_{1}.$

In short, by (9) $x_{0}y_{0}>k_{1}\lambda_{1}$, contradicting the fact that
$x_{0}y_{0}$ is least.

If the minus sign holds in (10c),

$y^{2}_{2}=-\rho_{1}k^{4}_{1}+2nk^{2}_{1}\lambda^{2}_{1}-\rho_{2}\lambda^{4}_{1}$
(10e)

Again, we use the fact that either $\rho_{1}=n^{2}-p$ and $\rho_{2}=1$ or
vice-versa.

In either case, $\rho_{1}+\rho_{2}=n^{2}-p+1$. Consider (10e) modulo 4. If
both $k_{1}$ and $\lambda_{1}$ are odd, then
$k^{2}_{1}\equiv\lambda^{2}_{1}\equiv 1\ ({\rm mod}\ 4)$ and so (10e) implies,

$\begin{array}[]{l}y^{2}_{2}\equiv-\rho_{1}+2n-\rho_{2}\equiv-(\rho_{1}+\rho_{2})+2n\equiv-(n^{2}-p+1)+2n\
({\rm mod}\ 4);\\\ \\\ y^{2}_{2}\equiv-n^{2}+p-1+2n\equiv 2\ ({\rm mod}\
4),\end{array}$

since by hypothesis $p\equiv 3\ ({\rm mod}\ 4)$ and $n$ is even. Thus, a
contradiciton.

If $k_{1}+\lambda_{1}\equiv 1\ ({\rm mod}\ 2)$, again consider (10e) modulo 4.
Given that $\rho_{1}=n^{2}-p$ and $\rho_{2}=1$ or vice-versa, and that $k_{1}$
is odd and $\lambda_{1}$ even, or vice-versa. The four combinations, because
of the symmetry of (10e) reduce to two congruence possibilities:
$y^{2}_{2}\equiv-1$ or $y^{2}_{2}\equiv-(n^{2}-p)\ ({\rm mod}\ 4)$, but
$n^{2}-p\equiv 1\ ({\rm mod}\ 4)$, by hypothesis . Therefore we see that in
both cases we arrive at $y^{2}_{2}\equiv 3\ ({\rm mod}\ 4)$ which is
impossible. This concludes the proof in subcase (2i).

Subcase 2(ii): Assume hypothesis (ii) of the theorem. Then $n^{2}-p<0$ and
$N=p-n^{2}$ is a prime. Combining (8) with (9a) and $2y_{1}y_{2}=y_{0}$ in (9)
leads to

$x^{2}_{0}=(y^{2}_{2}-2ny^{2}_{1})^{2}+(p-n^{2})(2y^{2}_{1})^{2}$ (11)

By (9) we know that $(y_{1},y_{2})=1$ and $y_{2}$ is odd; which implies that
$(y^{2}_{2}-2ny^{2}_{1},2y^{2}_{1})=1$. By (11), the triple
$\left(\left|y^{2}_{2}-2ny^{2}_{1}\right|,2y^{2}_{1},x_{0}\right)$ is a
positive integer solution to the diophantine equation $x^{2}+\ell
y^{2}=z^{2}$, with $\ell=p-n^{2}$; and with the integers
$\left|y^{2}_{2}-2ny^{2}_{1}\right|$ and $2y^{2}_{1}$ being relative prime.
Accordingly, by (2) we must have

$\left|y^{2}_{2}-2ny^{2}_{1}\right|=\dfrac{d(\rho_{1}k^{2}-\rho_{2}\lambda^{2})}{2},\
2y^{2}_{1}=dk\lambda;$

$\left\\{\begin{array}[]{l}y^{2}_{2}-2ny^{2}_{1}=\pm\dfrac{d(\rho_{1}k^{2}-\rho_{2}\lambda^{2})}{2},\
2y^{2}_{1}=dk\lambda,\\\ {\rm for\ positive\ integers}\
d,k,\lambda,\rho_{1},\rho_{2}\ {\rm such\ that}\\\ (k,\lambda)=1,\
\rho_{1}\rho_{2}=p-n^{2},\ {\rm and\ with}\ d=1\ {\rm or}\
2\end{array}\right\\}$ (12)

Since we consider (below) all the combinations $\rho_{1},\rho_{2}$ such that
$\rho_{1}\rho_{2}=p-n^{2}$, it follows that the plus or minus possibilities in
the first equation of (12) are really the same. Thus, we may write

$y^{2}_{2}-2ny^{2}_{1}=\dfrac{d(\rho_{1}k^{2}-\rho_{2}\lambda^{2})}{2},\
2y^{2}_{1}=dk\lambda$ (12a)

As we saw in the proof of subcase (ii), the possibility $d=1$ is easily ruled
out. Indeed, if $d=1$, the first equation in (12a) implies that the integer
$(\rho_{1}k^{2}-\rho_{2}\lambda^{2})$ must be even. On the other hand, the
second equation in (12a) implies, since $(k,\lambda)=1$ that $k$ must be odd
and $\lambda$ even; or vice-versa. But then, by virtue of the fact that
$\rho_{1},\rho_{2}$ are both odd, it follows that
$\rho_{1}k^{2}-\rho_{2}\lambda^{2}\equiv 1\ ({\rm mod}\ 2)$, a contradiction.
Thus, $d=2$ in (12a). We have,

$y^{2}_{2}-2ny^{2}_{1}=\rho_{1}k^{2}-\rho_{2}\lambda^{2},\ y^{2}_{1}=k\lambda$
(12b)

Obviously, the second equation in (12b) implies, since $(k,\lambda)=1$, that
$k=k^{2}_{1}$ and $\lambda^{2}_{1}=\lambda$ for some
$k_{1},\lambda_{1}\in{\mathbb{Z}}^{+}$, with $k_{1},\lambda_{1})=1$. Using
$y_{1}=k_{1}\lambda_{1}$ as well, we see that (12b) implies

$y^{2}_{2}=\rho_{1}k^{4}_{1}+2nk^{2}_{1}\lambda^{2}_{1}-\rho_{2}\lambda^{4}_{1}$
(12c)

Since $\rho_{1}\rho_{2}=p-n^{2}=$ prime, there are precisely two
possibilities. Either $\rho_{1}=1,\ \rho_{2}=p-n^{2}$ or, alternatively,
$\rho_{1}=p-n^{2}$ and $\rho_{2}=1$. In the first case, $\rho_{1}=1$ and
$-\rho_{2}=n^{2}-p=m$; so that by (12c),
$y^{2}_{2}=k^{4}_{1}+2nk^{2}_{1}\lambda^{2}_{1}+m\lambda^{4}_{1}$, which shows
that the triple $(k_{1},\lambda_{1},y_{2})$ is a positive integer solution to
the initial equation (1). Compare this solution with the solution
$(x_{0},y_{0},z_{0})$. We have, $x_{0}y_{0}\geq
y_{0}=2y_{1}y_{2}>y_{1}=k_{1}\lambda_{1}$, violating the minimality of the
product $x_{0}y_{0}$. Next, assume the next possibility to take hold, namely
$\rho_{1}=p-n^{2}$ and $\rho_{2}=1$. Then equation (12c) implies,

$y^{2}_{2}=(p-n^{2})k^{4}_{1}+2nk^{2}_{1}\lambda^{2}_{1}-\lambda^{4}_{1}$
(12d)

Consider (12d) modulo 4:

If $k_{1}\equiv\lambda_{1}\equiv 1\ ({\rm mod}\ 2)$, then (12d) implies
$y^{2}_{2}\equiv p-n^{2}+2n-1\ ({\rm mod}\ 4)\Rightarrow$ (since $n$ is even
and $p\equiv 3\ ({\rm mod}\ 4))\ y^{2}_{2}\equiv 2\ ({\rm mod}\ 4)$, an
impossibility.

If $k_{1}\equiv 0$ and $\lambda_{1}\equiv 1\ ({\rm mod}\ 2)$, (12d) implies
$y^{2}_{2}\equiv-1\equiv 3\ ({\rm mod}\ 4)$, again impossible.

Finally, if $k_{1}$ is odd and $\lambda_{1}$ even, (12d) implies
$y^{2}_{2}\equiv p-n^{2}\ ({\rm mod}\ 4);$ $y^{2}_{2}\equiv 3\ ({\rm mod}\
4)$, again an impossibility.

This concludes the proof of subcase (ii) and with it, the proof of the
theorem.

##  4 Numerical Examples

  1. (i)

Below, we provide a list of all combinations of positive integers $n,p,m$;
such that both $p$ and $m$ are primes, $m=n^{2}-p$, and with either $n\equiv
0\ ({\rm mod}\ 4)$ and $p\equiv 3\ ({\rm mod}\ 8)$, or alternatively, $n\equiv
2\ ({\rm mod}\ 4)$ and $p\equiv 7\ ({\rm mod}\ 8)$. Under the constraint
$n\leq 16$, there are 24 such combinations.

$\begin{array}[]{|r|c|c|c|}\hline\cr&n&p&m\\\ \hline\cr 1)&4&3&13\\\ \hline\cr
2)&4&11&5\\\ \hline\cr 3)&6&7&29\\\ \hline\cr 4)&6&23&13\\\ \hline\cr
5)&6&31&5\\\ \hline\cr 6)&8&3&61\\\ \hline\cr 7)&8&11&53\\\ \hline\cr
8)&8&59&5\\\ \hline\cr 9)&10&47&53\\\ \hline\cr 10)&10&71&29\\\ \hline\cr
11)&12&43&101\\\ \hline\cr 12)&12&83&61\\\ \hline\cr\end{array}\hskip
36.135pt\begin{array}[]{|r|c|c|c|}\hline\cr&n&p&m\\\ \hline\cr
13)&12&107&37\\\ \hline\cr 14)&12&131&13\\\ \hline\cr 15)&12&139&5\\\
\hline\cr 16)&14&23&173\\\ \hline\cr 17)&14&47&149\\\ \hline\cr
18)&14&167&29\\\ \hline\cr 19)&14&191&5\\\ \hline\cr 20)&16&59&197\\\
\hline\cr 21)&16&83&173\\\ \hline\cr 22)&16&107&149\\\ \hline\cr
23)&16&227&29\\\ \hline\cr 24)&16&251&5\\\ \hline\cr\end{array}$

  2. (ii)

Below, we provide a listing of all combinations of integers $n,p,m,N$; such
that $n,p,N>0,\ m<0,\ p$ and $N$ are both primes, $N=p-n^{2},\ m=-N,$ and with
either $n\equiv 0\ ({\rm mod}\ 4)$ and $p\equiv 3\ ({\rm mod}\ 8)$, or
alternatively, with $n\equiv 2\ ({\rm mod}\ 4)$ and $p\equiv 7\ ({\rm mod}\
8)$. Under the constraint $p\leq 251$, there are 29 such combinations.

$\begin{array}[]{|r|c|c|c|c|}\hline\cr&p&n&N&m\\\ \hline\cr 1)&7&2&3&-3\\\
\hline\cr 2)&23&2&19&-19\\\ \hline\cr 3)&47&2&43&-43\\\ \hline\cr
4)&47&6&11&-11\\\ \hline\cr 5)&59&4&43&-43\\\ \hline\cr 6)&67&8&3&-3\\\
\hline\cr 7)&71&2&67&-67\\\ \hline\cr 8)&79&2&73&-73\\\ \hline\cr
9)&79&6&43&-43\\\ \hline\cr 10)&83&4&67&-67\\\ \hline\cr 11)&83&8&19&-19\\\
\hline\cr 12)&103&6&67&-67\\\ \hline\cr 13)&103&10&3&-3\\\ \hline\cr
14)&107&8&43&-43\\\ \hline\cr 15)&131&8&67&-67\\\ \hline\cr\end{array}\hskip
36.135pt\begin{array}[]{|r|c|c|c|c|}\hline\cr&p&n&N&m\\\ \hline\cr
16)&163&12&19&-19\\\ \hline\cr 17)&167&2&163&-163\\\ \hline\cr
18)&167&6&131&-131\\\ \hline\cr 19)&167&10&67&-67\\\ \hline\cr
20)&179&4&163&-163\\\ \hline\cr 21)&199&6&163&-163\\\ \hline\cr
22)&199&14&3&-3\\\ \hline\cr 23)&211&12&67&-67\\\ \hline\cr
24)&227&4&211&-211\\\ \hline\cr 25)&227&8&163&-163\\\ \hline\cr
26)&227&12&83&-83\\\ \hline\cr 27)&239&10&139&-139\\\ \hline\cr
28)&239&14&43&-43\\\ \hline\cr 29)&251&12&107&-107\\\ \hline\cr&&&&\\\
\hline\cr\end{array}$

##  5 Historical Commentary

Mathematical research on diophantine equations of the form

$ax^{4}+bx^{2}y^{2}+cy^{4}=dz^{2}$ (13)

dates back to the early 17th century. The most comprehensive source of results
on such equations in the 300 year-period from the early 17th century to about
1920, is I. E. Dickson’s monumental book History of the Theory of Numbers,
Vol. II, (see [1]).

All or almost all results (at least the referenced ones) of that period can be
found in that book. Various researchers during that time period employed
decent methods to tackle such equations. Perhaps all the significant results
achieved in that 300-year period can be attributed to about 40-50
investigators. We list the names of thirty-two of them:

Fermat, Frenicle, St. Martin, Genocci, Lagrange, Legendre, Lebesgue, Euler,
Adrain, Gerardin, Aubry, Fauquenbergue, Sucksdorff, Gleizes, Mathieu, Moret-
Blank, Rignaux, Kausler, Fuss, Auric, Realis, Mantel, Desboves, Kramer,
Escott, Thue, Cunningham, Pepin, Lucas, Werebrusov, Carmichael, Pocklington.

A detailed account of the results obtained by these mathematicians is given in
[1], pages 615-639.

On the other hand, the last 75 years or so (from the early 1930’s to the
present) are marked by the introduction and development of what is known as
local methods as well as the connection/association of equations (13) with
elliptic curves. In particular, the beginning of the 75 year period (early
thirties) is characterized by a landmark, the Hasse Principle:

If $F\in{\mathbb{Z}}[x_{1},\ldots,x_{n}]$ is a homogenous polynomial of degree
$2$, then $F(x_{1},\ldots,x_{n})$ has a nontrivial solution in
${\mathbb{Z}}^{n}$ if, and only if,

    1. (a)

it has a nontrivial solution in ${\mathbb{R}}^{n}$ and

    2. (b)

it has a primitive solution modulo $p^{k}$ , for all primes $p$ and exponents
$k\geq 1$.

Here, a solution $(a_{1},\ldots,a_{n})$ is understood to be nontrivial if at
least one of the $a_{i}$’s is not zero. It is primitive if one of the
$a_{i}$’s is not divisible by $p$.

In 1951, E. Selmer (see [3]), presented an example of a homogenous polynomial
in three variables, and degree $n=3$ which fails the Hasse Principle.This is
the equation $3x^{3}+4y^{3}+5z^{3}=0$, whose only solution in
${\mathbb{Z}}^{3}$ is $(0,0,0)$ (so it has no nontrivial solutions). But it
obviously has nontrivial solutions in ${\mathbb{R}}^{3}$; and it has primitive
solutions modulo each prime power.

In their paper W. Aitken and F. Lemmermeyer, (see [4]), show that equation
(13) has a nontrivial solution in ${\mathbb{Z}}^{3}$ if, and only if, the
diophantine system (in four variables $u,v,w,z$)

$\left\\{\begin{array}[]{ll}{\rm with}\ b^{2}-4ac\neq
0,&au^{2}+bv^{2}+cw^{2}=dz^{2}\\\ \\\ {\rm and}\ d\ {\rm
squarefree},&uw=v^{2}\end{array}\right\\}$ (14)

has a nontrivial solution in ${\mathbb{Z}}^{4}$. This also holds when
${\mathbb{Z}}$ is replaced by any ring containing ${\mathbb{Z}}$. In
particular, it holds for ${\mathbb{R}}$.

Furthermore, (14) has a primitive solution modulo $p^{k}$ if, and only if,
(13) has a primitive solution modulo $p^{k}$; and $k\geq 2$. (If $p$ is not a
divisor of $d$, this can be extended to $k=1$.)

In 1940 and 1942 respectively, C.-E Lind and H. Reichardt, (see [5] and [6]),
found another counterexample to the Hasse Principle: the diophantine equation
(13) with $a=1,\ b=0,\ c=-17$, and $d=2$; that is the equation
$x^{4}-17y^{4}=2z^{2}$.

Aitken and Lemmermeyer generalized the Lind and Reichardt example by taking
$a=1,\ b=0,\ c=-q$, such that $q$ is a prime with $q\equiv 1\ ({\rm mod}\
16),\ d$ is squarefree, $d$ is a nonzero square but not a fourth power modulo
$q$, and $q$ is a fourth power modulo $p$ for every odd prime $p$ dividing
$d$. Thus, they obtained a family of diophantine equations (13) (or
equivalently, systems (14)) which fail the Hasse Principle. Their proofs of
the nontrivial insolvability (of each member of that family) in
${\mathbb{Z}}^{3}$ only involves quadratic reciprocity arguments. The harder
part is to give an elementary proof that the above equations have primitive
solutions modulo all prime powers.

Variants of the Hasse Principle, and the manner in which these principles
fail, can be found in a paper by B. Mazur (see [7]). Also, there is the
seminal work by J. Silverman (see [8]), which provides a comprehensive study
for the links between equations (13) and elliptic curves.

Alongside these developements of the last 75 years, there have been some
results obtained by elementary means only. For example, A. Wakulitz (see [9])
has offered an elementary proof that the diophantine equation
$x^{4}+9x^{2}y^{2}+27y^{4}=z^{2}$ has no solution in $({\mathbb{Z}}^{+})^{3}$.
A corollary of this (in the paper in [9]), is that the equation
$x^{3}+y^{3}=2z^{3}$ has no solution in ${\mathbb{Z}}^{3}$ with $x\neq y$ and
$z\neq 0$.

## References

     * [1] Dickson, L. E., History of the Theory of Numbers, Vol. II, Chelsea Publishing, Providence, Rhode Island, (1992), 803 pp. ISBN: 0-8218-1935-6
     * [2] Zelator, K., The diophantine equation $x^{2}+ky^{2}=z^{2}$ and integral triangles with a cosine value of $\frac{1}{n}$, Mathematics and Computer Education, Fall 2006.
     * [3] Selmer, E., The diophantine equation $ax^{3}+by^{3}+cz^{3}=0$, Acta Math. 85 (1951), 203-362.
     * [4] Aitken, W., Lemmermeyer, F., Counterexamples to Hasse Principle: An elementary introduction,
http://public.csusm.edu/aitken_html/m372/diophantine.pdf.

     * [5] Lind, C.-E, Untersuchungen über die rationalen Punkte der ebenen kubischen kurven vom Geschlect Eins, Diss. Univ. Uppsala 1940.
     * [6] Raichardt, H., Einige im Kleinen überall lösbare, im Grossen unlösbare diophantische Gleichungen, J. Reine Angew. Math. 184 (1942), 12-18.
     * [7] Mazur, B., On the passage from local to global in number theory, Bull. Amer. Math. Soc. (N.S.) 29 (1993), no. 1, 14-50.
     * [8] Silverman, J., The arithmetic of elliptic curves, Springer-Verlag 1986.
     * [9] Wakulitz, A., On the equation $x^{3}+y^{3}=2z^{3}$, Colloq. Math., 5 (1957), 11-15.


# Interactive Formal Specification
for Mathematical Problems
of Engineers

Walther Neuper Johannes Kepler University
Linz, Austria<EMAIL_ADDRESS>
###### Abstract

The paper presents the second part of a precise description of the prototype
that has been developed in the course of the ISAC project over the last two
decades. This part describes the “specify-phase”, while the first part
describing the “solve-phase” is already published.

In the specify-phase a student interactively constructs a formal
specification. The ISAC prototype implements formal specifications as
established in theoretical computer science, however, the input language for
the construction avoids requiring users to have knowledge of logic; this makes
the system useful for various engineering faculties (and also for high
school).

The paper discusses not only ISAC’s design of the specify-phase in detail, but
also gives a brief introduction to implementation with the aim of advertising
the re-use of formal frameworks (inclusive respective front-ends) with their
generic tools for language definition and their rich pool of software
components for formal mathematics.

##  1 Introduction

Since its beginnings more than two decades ago the ISAC project strives for a
generally usable system for mathematics education, which might cover a major
part of educational scenarios, posing and solving problems which can best be
tackled by mathematical methods. This paper presents the second part of a
concise description of the prototype that has been developed in the course of
the project, the description of the so-called specify-phase, while the first
part describing the solve-phase is already published [16].

The specify-phase first addresses the “what to solve”, while the solve-phase
addresses the “how to solve” later in the process of problem solving — an
important conceptual separation in the education of engineers. In terms of
computer mathematics the fist phase concerns a transition from facts in the
physical world (captured by text or figures) to abstract notions of
mathematics (mainly captured by formulas). And in terms of educational science
and psychology this first phase concerns a transition from intuitive and
associative human thinking to handling of abstract formal entities according
to formal logic.

A successful transition results in a “formal specification” (to be exactly
defined in §2.2 Pt.2 on p.2), so the subsequent solve-phase resides
exclusively in the abstract area of computater mathematics, where Lucas-
Interpretation [16] is able to automatically generate “next step guidance” [6]
and reliable checks of logical correctness — this paper, however, addresses
the preceding phase, more challenging in terms of computer mathematics and in
terms of psychology.

The latter point will be touched on in this paper only by relating it here to
recent advances in Artifical Intelligence, where ChatCPT for instance,
achieved great public attention, even among computer mathematicians [4]. A
software, which given a textual description of mathematical problems is able
to convincingly reason about relevant facts, to react to supplementary remarks
and even come up with a solution for the problem _and is able to justify the
solution_ — doesn’t it outperform software of formal mathematics, in
particular, might it outperform the ISAC prototype? In spite of this serious
question, the present step of development in the ISAC project continues to
build the prototype solely upon the proof assistant Isabelle [20]. Presently
without systematic experiments and detailed examination, the ISAC project is
aware, that integrations of AI technologies and formal mathematics are a vivid
research topic (see, for instance, [3, 10]). And the description of our
conservative approach contains hints at a “dialog guide” and a “user model”,
which will be necessary to adapt the power of the ISAC protoype (and system,
sooner or later) to the needs of the user, the student – and in such future
development the ISAC project will come back to AI.

The present description, of how the ISAC prototype handles the specify-phase,
is partly a position paper in that it omits the justification for user
requirements (already published in [17, 19, 18]) and not even evaluates them
(which shall be more informative in a broader educational setting in the
future). And partly the description reports technical details how design and
implementation attempts to realise these requirements; a secondary objective
of the description is to motivate the reuse of generic tools for language
definition in proof assistants and their rich pool of software components for
formal mathematics and also their front-ends — and _not_ to re-invent the
wheel again and again in educational math software development.

The paper has another special feature, the lack of related work — because
there seems none to be to the best knowledge of the author. The ThEdu workshop
series were founded to promote activities for the creation of software
generally useful for mathematics education. There have been notable successes
with geometry software and software to teach mechanical reasoning in academia,
but software to support learning in the most general education settings, maths
problem solving, still does not exist.

There is an actual reason for writing this paper now: It became apparent that
the Java-based front-end of the ISAC prototype cannot catch up with recent
development of front-ends in mathematics software: proof assistants make
semantic information transparent to the user, they make formulas a door open
for a great portion of mathematics knowledge just by mouse-click. So this lead
to the hard decision to drop the Java-based front-end, i.e. about thirty
valuable student projects 111https://isac.miraheze.org/wiki/Credits and to
start shifting ISAC’s code in between Isabelle’s proof machinery and
Isabelle’s upcoming new front-end Isabelle/VSCode. The first step in this
shift is additionally motivated by a lucky technical coincidence: Isabelle’s
formulas (terms, in respective diction) are _linear_ sequences of (very
specific) characters – and so are formulas on the Braille
display222https://en.wikipedia.org/wiki/Refreshable_braille_display. Thus ISAC
engages in the “A-I-MAWEN” project aiming at an Accessible
333https://en.wikipedia.org/wiki/Accessibility and
Inclusive444https://en.wikipedia.org/wiki/Inclusion_(education) Mathematics
Working Environment taking advantage from VSCode’s accessibility features; and
Isabelle enjoys collaboration on its upcoming new new front-end [12, 24].

#### The paper is organised as follows.

After the introduction first come user requirements, as clarified in the ISAC
project. The requirements are partitioned in general ones in §2.1 and ones
addressing the specify-phase in §2.2.

After a definition of “formal specification” the design of interaction in the
specify-phase is described by use of a running example given in §3.1. §3.2
describes the transition from text and figures into formal mathematics, §3.3
turns to the most essential features, freedom in input and freedom to
pursuevariants in problem solving. §3.4 shows, what kinds of feedback can be
given in the specify-phase. And §3.5 addresses problem-refinement, a
particularly sketchy part in the ISAC prototype. The final section §3.6
concerns the transition from the specify-phase to the solve-phase.

Since the paper also wants to advertise the generic tools of proof assistants
for defining new input languages, in particular the tools of Isabelle, the
section on implementation is detailed as follows. §4.1 shows how elegantly
ISAC’s input language for the specify-phase can be implemented in
Isabelle/Isar, §4.2 goes into detail with handling semantics of the input.
Analogously to the solve-phase also the specify-phase is organised in steps
introduced in §4.3. A specific detail is refinement of equations discussed in
§4.4. §4.5 addresses efficiency considerations and finally in §4.6
preconditions are described, which require evaluation by rewriting. §5 gives a
brief summary and concludes the paper.

##  2 User Requirements

ISAC aims at an educational software and so design and development started
with analysing the requirements, which a student places on the system when
using it according to the introduction. The requirements capture and
requirements analysis in the ISAC project
555https://isac.miraheze.org/wiki/History are already published in [17, 19,
18]. Here the requirements 666This list will go into the ISAC documentation
and supersedes the old documentation [21]. are kept as short as possible, are
restricted to the specify-phase and serve to introduce the system features
from the users point of view; the descriptions of respective implementation
details in §3 justify the requirements more or less explicitly by backward
references. However, first come some general considerations.

###  2.1 Foundational axioms about User Requirements

ISAC’s decision to build software on top of reasoning technology – for maths
education at high school and academic engineering courses, this decision is
novel and opens up novel educational settings. The efficiency of these setting
shall be researched thoroughly. As soon as tracing data777There are good
experiences with logging user-interaction in ISAC [11] from the interaction
with such tools become available, interesting discussions in educational
research of mathematics education can be expected.

Until then the following requirements are considered as abstract and so far
from concrete usability testing that these requirements are stated as axioms,
axioms advocating software models to learn by interaction, _not_ to learn by a
teachers explanation primarily:

  * •

A complete model of mathematics shall comprise all software tools required to
solve a problem at hand, such that a student need not switch between different
software applications: the problem statement, the textbook with background
theory and explanation, the formulary, probably another textbook with a
boilerplate for solving the problem at hand, and last not least an electronic
notebook for interactive construction of a solution for the problem.

  * •

A transparent model of mathematics shall be open for all kinds of inquiry of
the underlying maths knowledge: What data is required to probably describe a
given problem? What is required as input, what is expected as output? What are
the types of the respective data types? What are the constraints
(preconditions) on the input? What pattern does the problem at hand match,
what are similar problems? And at the transition to the solve-phase there are
further questions to be answered by the system: Which methods could be
appropriate for finding a solution? Etc.

  * •

An interactive model of mathematics shall support step-wise construction of a
solution to a given problem. Each step is checked for correctness and
justified according to the above axiom of “transparency”. So interaction
follows the principle of “correct by construction”.

ISAC’s basic design is not embossed to mimic a human lecturer or teacher,
rather the student shall learn independently from a software model, which
clearly represents an essence of mathematics. In fact, if mathematics is the
“science to mechanise thinking” (Bruno Buchberger
888https://en.wikipedia.org/wiki/Bruno_Buchberger), then this science is most
appropriate one to be modelled on computers, essentials can be best studied
there and prover technologies provide the most powerful tools [15] for
developing tools, which give justifications and explanations.

Experiences with ISAC indicate that the hint of “mechanises thinking” is
helpful for students at any age, helpful to chase the omnipresent suspicion
that mathematics is magic. Just watch a power user of a proof assistant, how
she or he plays around with text snippets in order to find solutions (after a
coarse idea of a subject matter or a proof has become clear).

###  2.2 User Requirements focusing Specify-Phase

Now, what follows are the requirements which serve to pass the specify-phase
successfully, to come from human imagination of a problem (triggered by an
informal text or a figure or whatever) to a formal representation, appropriate
to be tackled within software.

  1. 1.

As an educational software ISAC must be intuitive such that a newbie can
easily learn to use the system by interacting with trial and error.

  2. 2.

The system ensures “correctness by construction” when given a formal
specification (definition): Two lists of terms are given, input $\it{in}$ and
output $\it{out}$. And given are two predicates: The precondition
$\it{Pre}\;(\it{in})$ constrains the elements of the input to reasonable
values. The postcondition $\it{Post}\;(\it{in},\,\it{out})$ relates input and
output (and thus characterises the kind of problem).

This definition is according to [9] and restricts the kind of problems
accepted by the system.

  3. 3.

If a student gets stuck, the system can propose a next step, i.e. a single
element of the specification, which is still missing (equivalent to Lucas-
Interpretation [16]).

  4. 4.

ISAC tries to raise students awareness of different operational power in
different number ranges (e.g. in the complex numbers each polynomial has
roots, in the real numbers it may have none). Thus it restricts Isabelle’s
contexts to particular theories, for instance to Int.thy, to Real.thy or to
Complex.thy.

  5. 5.

No need for formal logic: The formal specification of a problem must be
comprehensible for students in an academic course in engineering disciplines
(and also at high school) without any instruction in formal logic. So a
_Specification_ is given by _Given_ (the input according to Pt.2), _Where_
(the precondition) and _Find_ (the output, i.e. the solution of the problem)
and _Relate_ (to be described in the next point).

  6. 6.

_Relate_ captures essential parts of the postcondition such that the
description avoids logical operators (like $\exists$, $\forall$, $\land$,
$\lor$ etc) according to requirement UR.5. This is a crucial design decision
of ISAC which will be illustrated by the running example.

  7. 7.

In general, mathematical problems can be solved in many ways. Thus a
_Specification_ must be open for variants which are handled within one and the
same process of solving the problem. The running example (§3.3 below)
illustrates three variants.

  8. 8.

The transition from an informal problem description, given by text and by
figures, to the formal specification must not be overstrained by issues of
formal notation. The problem is well-known from educational use of algebra
systems [8]. Thus ISAC will give the following templates for the respective
types (examples are given in Fig.1 below):

     * •

$[$__=__, __=__$]$ for lists of equalities, for example ${\it
Constants}\,[a=1,b=2]$

     * •

$[$__, __$]$ for lists of elements without $=$, for example ${\it
AdditionalValues}\,[a,b,c]$

     * •

”__” for theories (as strings), for example ${\it
Theory\\_Ref}\;{\it"Diff\\_App"}$

     * •

”__/__” for string lists, for example ${\it
Problem\\_Ref}\;{\it"univariate\\_calculus/optimisation"}$

     * •

__ for arbitrary input (not involving the above cases), for example ${\it
Maximum\;A}$.

  9. 9.

Within the _Specification_ the _Model_ serves two purposes: for the
_Problem_Ref_ it shows the fields from _Given_ to _Relate_ according to Pt.5
and for _Method_Ref_ it shows the guard of the program guiding the _Solution_
; for details see [16]. A toggle switches between the two purposes (in the
examples below indicated by $\otimes$ and $\odot$, the former for activation
and the latter for idle).

  10. 10.

The specify-phase can be skipped on predefined settings. This requirement is
more important than it seems: ISAC may be not only be used for solving new
problems, but also for exercising _known_ problems, for instance
differentiation. In that case _Specification_ will be folded in such that the
solve-phase will be started immediately by _Solution_.

  11. 11.

A _Specification_ can be completed automatically (by pushing a button or the
like), in case a student wants to enter the solve-phase right now (and in case
the course designer allows to do so by the predefined settings).

  12. 12.

In equation solving the system can assist in finding an appropriate type of
equation. That means, in this special case the system is capable of problem
refinement (which is under ongoing research on more general problem types).
The user requests this assistance by easy-going means (by pushing a button or
the like).

  13. 13.

There is the following feedback on a specification’s elements, indicated at
the appropriate location of the respective element on screen:

     * •

Correct: There is probably no specific indication.

     * •

Syntax: This feedback can be necessary, if the user switches the _Model_
suddenly from _Problem_Ref_ to _Method_Ref_ or vice versa, see UR.9

     * •

Incomplete: Input is incomplete, in particular elements of type list.

     * •

Superfluous: An input can be syntactically correct, but have no evident
relation to the problem at hand.

These user requirements evolved alongside two decades of development in the
ISAC project, which was close to educational practice all the time due to the
involved persons; and the requirements have been checked in several field
tests [17, 19, 18].

The requirements raise a lot of questions with respect to detailed software
design. Some of the questions will be clarified alongside presenting the
running example in §3 below.

##  3 Design of the Specify-Phase

In the specify-phase a student interactively constructs a formal specification
(definition in §2.2 Pt.2 on p.2), which then enables Lucas-Interpretation [16]
to automatically generate user guidance. The concept of formal specification
involves logic, which is not taught at many engineering faculties (and not at
all at high school), however. Thus, according to §2.2 requirement no.2 on p.2,
respective logic is hidden from the user; for explaining that approach we use
a running example.

###  3.1 A Running Example

The running example is re-used from [12]: There it was used to illustrate what
has been achieved in the old prototype and what is _planned_ for developing a
“mathematical working environment”, whereas in this paper the example is used
to explain the design and implementation of the part of the prototype
supporting the specify-phase.

The efficiency of an electrical coil depends on the mass of the kernel. Given
is a kernel with cross-sectional area, determined by two rectangles of the
same shape as shown in the figure.
Given a radius $r=7$, determine the length $u$ and width $v$ of the rectangles
such that the cross-sectional area $A$ (and thus the mass of the kernel) is a
maximum.

In ancient times this kind of example belonged to a well-established class of
examples at the end of the mathematics curriculum at German speaking
Gymnasiums, “Extremwertaufgaben”. Nowadays it can be found in text books for
electrical engineering.

###  3.2 Formalisation of Problems and Authoring

In order to meet UR.3 it is necessary to prepare data for each example, where
automated generation of user guidance is desired [14]. Classes of examples are
collected to Problems; this conforms with teaching experience: certain classes
focus on certain problem patterns, which are explained and exercised by more
or less different examples.

Most of the lecturers and teachers want to expose their _personal_ collection
of exercises to their students; so lecturers should be enabled to implement
these independently in the system, without further expertise – so _authoring
for lecturers_ needs to be supported eventually for type Formalise.T below.
However, the implementation of problem patterns Model_Pattern.T involves
specific knowledge in computer mathematics – so _maths authoring_ needs to be
supported in addition, eventually. “Maths authors” might be lecturers of
specific academic courses, book authors and others.

According to this distinction there are the following two data-types 999We
adapt ML [13] syntax for readability purposes: instead of ”type T in structure
Formalise” we write ”Formalise.T”. ”(*” and ”*)” enclose comments, which are
outside ML syntax. The numbers on the left margin serve referencing and do not
belong to the ML code.:

    01  type Formalise.T = model * refs;

    01  type Model_Pattern.T =
    02    (m_field *        (* field "Given", "Find", "Relate"   *)
    03      (descriptor *   (* for term                          *)
    04        term))        (* identifier for instantiating term *)
    05    list;
    06  (*does NOT contain preconditions "Where"; these have no descriptor*)

The type Formalise.T consists of a (preparatory form of) model and refs; the
latter are explained below in §3.6. Model_Pattern.T is designed according to
UR.5. Each term is accompanied by a descriptor, which informs the user about
what is requested from him to input. Pairs of (descriptor * term) are assigned
to m_fields according to UR.5. The special values for the running example are
as follows, where the descriptors are Constants, Maximum, AdditionalValues,
Extremum, SideConditions, FunctionVariable, Domain and ErrorBound:

    01  val demo_example = ("The efficiency of an electrical coil depends on the mass
                             of the kernel. Given is a kernel with cross-sectional area
                             determined by two rectangles of same shape as shown in the
                             figure. Given a radius r = 7, determine the length u and
                             width v of the rectangles such that the cross-sectional
                             area A (and thus the mass of the kernel) is a maximum.
                             + Figure",
    02     ([
    03     (*Problem model:*)
    04       "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
    05       "Extremum (A = 2 * u * v - u \<up> 2)",
    06       "SideConditions [((u::real) / 2) \<up> 2 + (v / 2) \<up> 2 = r \<up> 2]",
    07       "SideConditions [(u::real) / 2 = r * sin \<alpha>, v / 2 = r * cos \<alpha>]",
    08     (*MethodC model:*)
    09       "FunctionVariable u", "FunctionVariable v",
    10       "FunctionVariable \<alpha>",
    11       "Domain {0 <..< r}",
    12       "Domain {0 <..< \<pi> / 2}",
    13       "ErrorBound (\<epsilon> = (0::real))"]: TermC.as_string list,
    14      ("Diff_App", ["univariate_calculus", "Optimisation"],
    15        ["Optimisation", "by_univariate_calculus"]): References.T)): Formalise.T

The text in line 01 exceeds the line limit, it has already been shown with the
problem statement of the running example in §3.1. The reader may be surprised
by the multiple entries for the descriptors SideConditions, FunctionVariable
and Domain; this is due to _variants_ introduced in §3.3 below — this
representation of variants is considered intermediate, it was easy to
implement and will be up to further refinement. The lines 14 and 15 represent
the refs introduced above in Formalise.T and explained in §3.6 below. The
attentive reader will also notice that the items of the example’s model are
not assigned to an m_field (line 02 on p.3.2), rather the descriptor is the
means to relate items between different data structures, in this case between
Formalise.model and the problem below defining the running example:

    01  problem pbl_opti_univ : "univariate_calculus/Optimisation" =
    02    \<open>eval_rls\<close> (*for evaluation of 0 < r*)
    03    Method_Ref: "Optimisation/by_univariate_calculus"
    04    Given: "Constants fixes"
    05    Where: "0 < fixes"
    06    Find: "Maximum maxx" "AdditionalValues vals"
    07    Relate: "Extremum extr" "SideConditions sideconds"

The above problem assigns the elements of the model (in ISAC we call an
element of a model an _item_ in order not to confuse with _elements_ of lists
or sets) to a respective m_field. As already mentioned, the assignment is done
via descriptors accompanied with place-holders (fixes, maxx, etc; see line 03
in type Model_Pattern.T on p.3.2) – these are instantiated on the fly with
values of the concrete example selected by the user.

It is the task of a mathematics author to decide the structure of the model
such that it covers an appropriate collection of examples, where a respective
Model_Pattern.T of a problem is instantiated for several examples by values of
a Formalise.T. For instantiation of the model for a problem an environment is
required, for instance for the demo_example the environment

[ | $("fixes",\;[r=7]),\;\;("maxx",\;A),\;\;("vals",\;[u,v]),$
---|---
| $("extr",\;(A=2*u*v-u\uparrow 2)),\;\;("sideconds",\;[(u/2)\uparrow
2+(v/2)\uparrow 2=r\uparrow 2])$
]

is required.

Another reason for this late assignment is that one and the same item may
belong to m_field Relate for a problem but to Given for a method, see §3.6.
Finally it may be remarked that the identifier
"univariate_calculus/Optimisation" can be found in a more convenient format
already on p.3.2 on line 14).

###  3.3 Freedom of Input and Variants in Problem Solving

The model described above is presented 101010§4.1 will show how easily the
format presented in the screen-shot can be defined in Isabelle/Isar. to
students as shown in the screen-shot below.

Figure 1: The template for starting a _Specification_.

There the descriptors (Constants, etc) are followed by templates giving hints
on the input format according to UR.8 in order to help students to cope with
the troublesome transition to exact formal representation. The Model is
embedded into the Specification which also contains References explained in
§3.6 below. The above template is completed in Fig.2 on p.2 and the reader may
refer to the Relate in the Model when reading the next paragraph.

##### Representation in field Relate is simplified

such that a student needs not encounter formal logic according to UR.6. Fig.2
shows that for the demo_example Extremum and SideConditions actually are the
essential parts of the postcondition, which characterises a problem by
relating Given and Find:

$\displaystyle(A=2*u*v-u\uparrow 2)\;\;\land\;\;((u/2)\uparrow 2+(v/2)\uparrow
2=r\uparrow 2)\;\;\land$ $\displaystyle\forall A^{\prime}u^{\prime}v^{\prime}$
. $\displaystyle(A^{\prime}=2*u^{\prime}*v^{\prime}-u^{\prime}\uparrow
2)\;\land\;((u^{\prime}/2)\uparrow 2+(v^{\prime}/2)\uparrow 2=r\uparrow
2)\;\;\Rightarrow A^{\prime}<A$

Students at engineering faculties usually are not educated in formal logic
(computer science is an exception). A formula containing $\land$ or
$\Rightarrow$ would distract them from actual problem solving. Thus ISAC
decided to extract the essential parts of the postcondition:

Extremum $(A=2*u*v-u\uparrow 2)$, SideConditions $(u/2)\uparrow
2+(v/2)\uparrow 2=r\uparrow 2$
---

These parts also are sufficient to automatically generate user-guidance
according to UR.3 (by enabling Lucas-Interpretation [14] to find a next step).

Input should not only be easygoing with respect to format and with bypassing
formal logic. According to UR.7 the system should cope flexibly with
semantics, it should also adapt to fresh ideas of a student and support
various variants in solving a particular problem. Let us look at Fig.2 with
the completed Specification and ask an important question:

Figure 2: The complete _Specification_.

What could a student have in mind when encountering the problem statement on
p.3.1? Looking at the figure on p.3.1, he or she might focus on the width $u$
and the length $v$, and apply Pythagoras theorem $(u/2)\uparrow
2+(v/2)\uparrow 2=r\uparrow 2$. But students might focus as well on the angle
$\alpha$ and formalise the SideConditions as
$u/2=r*\sin\alpha,\;v/2=r*\cos\alpha$.

And what if a student has an eye for simple solutions and takes as
SideConditions either $u=\cos\alpha,v=\sin\alpha$ or $u\uparrow 2+v\uparrow
2=4*r\uparrow 2$ ? The latter is semantically equivalent (equivalent in this
specific example) to the variant shown in Fig.2. So, during the whole specify-
phase, each formula input by a student must be checked for equivalence with
the formulas prepared in the Formalise.T. Such checking is done via rewriting
to a normal form. This might be quite tedious, for instance with equations
involving fractions like in showing equivalence of the equations $u\uparrow
2+v\uparrow 2=4*r\uparrow 2\;\equiv\;(\frac{u}{2})\uparrow
2+(\frac{v}{2})\uparrow 2=r\uparrow 2$)

#### An open design question, a “pattern-matching-language” ?

Now we are ready to address the design decision related to the format given on
p.3.2, which has been identified as preliminary and simplistic for the purpose
of simple implementation. Much information is redundant there, apparently, and
on the other hand interesting structural properties are hardly visible. For
instance, the student’s decision whether to take the FunctionVariable u or the
FunctionVariable v for differentiation (see §3.6), this decision is fairly
independent from the problem’s model – the Model just must no refer to
$\alpha$.

The need for a separated language for Specification becomes definitely clear
when considering the precondition and the postcondition (the latter introduced
above on p.3.3). The precondition must evaluate to true for a Specification to
be valid, and the postcondition must be true for a Solution to be accepted by
the system.

In order to evaluate precondition Where $0<r$ to true, we need to create the
environment $[(r,7)]$ from Constants. With the demo_example this is straight
forward, but if we had Constants [s = 1, t = 2] we already need to employ some
trickery with indexing. And what about the postcondition?

|  ${\it extr}\;\;\land\;\;{\it sideconds}\;\;\land$
---|---
$\forall\;\;{\it maxx}^{\prime}\;\;funvar^{\prime}.\;\;$ |  ${\it extr}^{\prime}\;\land\;{\it sideconds}^{\prime}\;\;\Rightarrow{\it maxx}^{\prime}<{\it maxx}$

How could such a “pattern-matching” description be instantiated to the
postcondition on p.3.3? Instantiated reliably, such that Isabelle could
evaluate it to true with the values found by Solution? How would the variant
with the $\alpha$ work out, which has two SideConditions?

Answering the open question above may go in parallel to implementation of a
larger body of examples and respective problems. Field tests [19, 17, 18] in
the ISAC project were based on limited content and thus did not gain much
experience with a variety of problems with variants and respective flexibility
of the system; one has to wait for implementation of more various examples and
problems.

###  3.4 Interactivity and Feedback

The previous section describes how ISAC makes a Specification flexible and
open for various variants in solving a particular problem. Flexibility in
problem solving must be accompanied by flexible interactivity and appropriate
feedback. Feedback for input to a Model is predefined by UR.13 and modelled by
a respective datatype as follows (values are of type term list)

    01  datatype I_Model.feedback =
    02      Correct of (descriptor * values)     (* wrt. syntax and semantics    *)
    03    | Incomplete of (descriptor * values)  (* for list types               *)
    04    | Superfluous of (descriptor * values) (* not found in Formalise.model *)
    05    | Syntax of TermC.as_string            (* in case of switching model   *)

The above code plus comments appear fairly self-explaining. descriptor has
been introduced already. In case of empty input, we shall have Incomplete (_,
[]) and display templates for input-format according to UR.8. Syntax errors
are handled very elegantly in Isabelle/PIDE (see §4.1); in case of switching
from the Model of the Problem_Ref to the Model of the Method_Ref (see §3.6
below) it might be useful to keep a copy of an input with syntax errors. Items
can be Superfluous either because they are syntactically correct but not
related the Model under construction, or they belong to a variant, which has
not yet been decided for. For instance, if the Model is as in Fig.2 on p.2 and
the student adds SideConditions $[v=\sin\alpha]$, this item will be marked as
Superfluous unless interactive completion to SideConditions
$[v=\sin\alpha,v=\cos\alpha]$ and deletion of a competing item like
SideConditions $[u\uparrow 2+v\uparrow 2=4*r\uparrow 2]$.

If a student gets stuck during input to a Model, then UR.3 allows him or her
to request help. In the specify-phase such help is given best by presenting a
(partial – predefined setting!) missing item. _But output of a Model with item
does not conform to Isabelle’s document model_: The content of an Isabelle
theory is considered a document which has to be checked by the system —
Isabelle is in principle a reactive system. There are few exceptions to the
document model, for instance, when Sledgehammer [5] finds intermediate proof-
steps on request and metis
111111https://isabelle.in.tum.de/library/HOL/HOL/Metis.html displays the
respective proof steps.

ISAC, in contrary, is designed as a tutoring system, where partners construct
a Specification and a Solution in cooperation, where the user can propose a
step while the system checks it and where the student can request help such
that the system can propose a step as well. Since here psychology of learning
is involved, a “user guide” component shall be involved in the future, and a
“user model” shall provide personalisation. ISAC’s original architecture
placed the components at the center of the system. But now ISAC is being
embedded in Isabelle and Isabelle/PIDE is already highly elaborated — where
will be the place for these components in Isabelle? This is one of the major
open questions for §4.

###  3.5 Automated Specifications

Sometimes a user might not be interested in specification. For instance, when
solving an equation, the type of the problem and the respective
Model_Pattern.T are clear, and only the hierarchy of problem types would have
to be searched for the appropriate type.

ISAC’s old Java front-end had a so-called CAS-command for that situation,
where one had minimal input, for instance $\it{solve\;(12-6\cdot x=0,\;x)}$.
Then ISAC checked the most general precondition (an “$=$” in the input) and
then started a breadth-first search in the tree of equations at the root
“univariate”, checking in sequence the type of the input term, linear, root,
polynomial, rational, complex or transcendental. Fig.3 shows the currently
available equations presented by the old Java fron-end.

Figure 3: The tree of equations (middle panel).

All these panels shall be redone by Isabelle/PIDE via Isabelle/VSCode.

The more interesting question is, whether this coarse refinement via
preconditions can be generalised to a kind of matching, which involves also
the postcondition (see p.3.3); theoretical background would most likely be the
refinement calculus [2].

###  3.6 Transition to the Solve-Phase

The solve-phase tackles the construction of a Solution for a given problem,
where “next-step-guidance” is provided by Lucas-Interpretation [16]. For that
purpose Lucas-Interpretation uses a program, and for such a program the values
specified by a Model instantiate the formal arguments of the program to actual
arguments. So items move from Relate to Given and new items need to be added
to the program’s guard in order to provide the program with all data required
for automatically construct a Solution. Thus the Model for the guard of the
demo_example might look as shown in Fig.4 below.

Figure 4: The Model for the Method_Ref.

The reader might notice that the toggle $\odot\otimes$ has changed, indicating
that the Model belongs to the Method_Ref (The toggle is not implemented
presently and just reminded of by a comment).

So the References come into play, they raise lots of open design decisions: We
encounter insightful _references_ into huge data collections; their
representation will heavily depend on specific features of VSCode (while the
structure of theories, DAGs, has not even an interactive representation
presently). Should they be collapsed by settings, if they would distract a
certain class from problem solving? Should students be forced to input
References, and when?

A reasonable intermediate step in development might be that a Model could be
accepted as complete (e.g. Fig.2) by the system even with empty References
(e.g. Fig.1) and a Solution could be started.

Toggling the Model between Model_Ref and Method_Ref (the former shown in Fig.2
on p.2, the latter in Fig.4) will be a challenge for implementation in
Isabelle/VSCode.

##  4 Implementation in Isabelle/Isar

This paper also intends to demonstrate that it is waste of resources to start
development of educational math software from scratch – nowadays users
expectations on software are high such that an isolated development cannot
keep pace with the still rapidly evolving state of the art. This is
particularly true for front-end technology. ISAC’s long lasting experience
with formula editors clearly demonstrates that unpleasant fact, which enforced
ISAC to drop ten years of front-end development.

This section is going to demonstrate simplicity of implementing a specific
input language as introduced in §3 above in one of the advanced proof
assistants, in this case Isabelle. Isar [23] is the proof language of Isabelle
and remarkably, this is defined in a generic manner such that almost arbitrary
formal languages can be defined; for a particularly interesting example see
[7].

###  4.1 Isabelle’s Outer and Inner Syntax

Isabelle separates two kinds of syntax, an inner syntax for mathematical terms
and an outer syntax for Isabelle/Isar’s language elements. The latter is
generic such that it allows for definition of various language layers. And it
is a pleasure to show how easily an ISAC Specification is defined such that
all inner syntax errors are indicated at the right location on screen, i.e.
how easily all what is shown in the screen-shots on the previous pages are
implemented such that syntax errors are shown appropriately:

    01  keywords "Example" :: thy_decl
    02    and "Specification" "Model" "References" "Solution"

The above two lines prepare Isar to re-use available parsers 121212In spite of
Isabelle’s convenient latex extensions we still use verbatim, which displays
“keyword$<$Specification$>$” as clumsily as
“keyword\$<$open$>$Specification\$<$close$>$”:

    01  Outer_Syntax.command command_keyword\<open>Example_TEST\<close>
    02   "prepare ISAC problem type and register it to Knowledge Store"
    03   (Parse.name -- Parse.!!! (keyword\<open>Specification\<close> --keyword<:> --
    04     keyword<Model> -- keyword<:> |-- Problem.parse_pos_model_input --
    05      (keyword<References> -- keyword<:> |-- Parse.!!! References.parse_input_pos
    06       )) >>
    07    (fn (example_id, (model_input,
    08      ((thy_id, thy_pos), ((probl_id, probl_pos), (meth_id, meth_pos))))) =>
    09     Toplevel.theory (fn thy =>
    10       let
    11         val state = update_step example_id model_input
    12           ((thy_id, thy_pos), ((probl_id, probl_pos), (meth_id, meth_pos)))
    13       in set_data state thy end)));

With these two definitions done, one has in update_step only to provide
appropriate calls of this function:

    01  fun term_position ctxt (str, pos) =
    02    Syntax.read_term ctxt str
    03      handle ERROR msg => error (msg ^ Position.here pos)
    04      (*this exception is caught by PIDE to show "msg" at the proper location*)

The exception ERROR is caught by Isabelle/PIDE and, for instance, syntax
errors detected by Syntax.read_term are displayed at the proper locations on
screen together with msg. _That is all what Isar requires to check syntax of
input as shown in the screen shots in the previous section and to indicate
errors at the proper location on screen._

The handling of _semantic_ errors is accomplished with Isabelle/ML, Standard
ML [13] enriched with an abundant collection of tools for formal logic as well
as for connection to the front-end via Isabelle/PIDE [22]. This will be shown
in the sequel.

###  4.2 Interaction and Feedback

Checking semantic appropriateness of user input to a Specification as
described in §3 above, comprises a lot of questions: Does an item input to a
Model belong to this particular example or is it just Superfluous? If there a
list is to be input, are all the elements present or are some missing (items
are Incomplete)? Is a Model complete with respect to a specified Problem_Ref?
If Theory_Ref is input, are all the items of a Model still parsed correctly
(or can, for instance, $"\it{Re}\,a+\it{Im}\,b")$ not be parsed correctly,
because the specified theory does not know the type “complex”)? Etc.

The central device for handling feedback to the above questions is the so-
called
INTERACTION_MODEL with the type I_Model.T 131313In ISAC’s code this definition
is shifted into a separate structure Model_Def _before_ the definition of the
store of a calculation, Ctree, which still lacks type polymorphism (where
variants is a list of integers and m_field has been introduced by type
Model_Pattern.T on p.3.2). Position.T establishes the reference to the
location on screen:

    01  type I_Model.single =
    02    variants *         (* pointers to variants given in Formalise.model *)
    03    m_field *          (* #Given | #Find | #Relate                      *)
    04    (feedback *        (* state of feedback for variables and values    *)
    05      Position.T);     (* for pushing feedback back to PIDE             *)

    06  type I_Model.T = I_Model.single list;

feedback implements UR.13 and resembles the structure of datatype feedback in
the presentation layer as shown on p.3.4 in §3.4. The first three characters
suffice for internal naming:

    01  datatype I_Model.feedback =
    02    Cor of (descriptor *         (* a term identifying an item          *)
    03       (values))                 (* of a particular example             *)
    04  | Inc of (descriptor * values) (* incomplete lists/sets,
                                          if empty then output according to UR*)
    05  | Sup of (descriptor * values) (* input not found Model               *)
    06  | Syn of TermC.as_string       (* kept for P_Model.switch_pbl_met     *)

###  4.3 Step-wise Construction of Specifications

Step-wise construction is one of the axioms for ISAC’s design as captured on
p.• ‣ 2.1. While step-wise construction appears self-evident for the solve-
phase, where Lucas-Interpretation suggests or checks one input formula after
the other, this appears artificial for the specify-phase: one can input any
item to a Specification in any sequence, items of a Model as well as
References. But there is also UR.3, which calls for the system’s ability to
propose a next step – and here we are:

    01  datatype Tactic.input =
    02  (* for specify-phase *)
    04    Add_Find of TermC.as_string                         (*add to the model*)
    05  | Add_Given of TermC.as_string  | Add_Relation of TermC.as_string
    06  | Model_Problem (*internal*)
    07  | Refine_Problem of Problem.id                (*refine a Model_Pattern.T*)
    08  | Refine_Tacitly of Problem.id (*internal*)
    09  | Specify_Method of MethodC.id                      (*specify References*)
    10  | Specify_Problem of Problem.id | Specify_Theory of ThyC.id
    11  (* for solve-phase *)
    12  | ...

The above Tactics are shown to the user, while some are used only internally;
Refine_* will be introduced in §4.4 below. A variant stuffed with lots of data
serve internal construction of a next step; the lists below shows only some
examples:

    01  datatype T = Add_Find’ of TermC.as_string * I_Model.T
    02  | Add_Given’ of TermC.as_string * I_Model.T
    04  | Add_Relation’ of TermC.as_string * I_Model.T
    05  | Model_Problem’ of                   (*starts the specify-phase     *)
    06      Problem.id *                      (*key to a Problem.T Store.node*)
    07      I_Model.T *                       (*model for the Problem        *)
    08      I_Model.T                         (*model for the MethoC         *)
    09  | Refine_Problem’ ...

###  4.4 Refinement of Problems

UR.12 calls for refinement, a respective motivation was given in §3.5. Here
implementation details are presented, because the subsequent section will
address efficiency consideration raised by refinement 141414By the way, Lucas-
Interpretation [16] is straightened considerably when equation solving in sub-
problems automatically refines to the appropriate type of equation.

A Problem.T is defined in an Isabelle theory; here the definition of the
model-pattern of the running example is shown.

Figure 5: The problem-pattern for the running example.

This model-pattern covers almost all examples of a well-known text book, the
items are identified by the descriptors; variables like fixes are to be
instantiated from a Formalise.model as explained on p.3.2. The convenient
representation in Fig.5 is stuffed with data required to solve a problem (see,
for instance, the $<$eval_rls$>$) and expanded to the type Problem.T:

    01  type Problem.T =
    02    {guh : Check_Unique.id,             (* unique within Isac_Knowledge   *)
    03    mathauthors : string list,          (* copyright etc                  *)
    04    start_refine : References_Def.id,   (* to start refinement with       *)
    05    thy  : theory,                      (* allows to compile model, where_*)
    06    cas : term option,                  (* CAS_Cmd                        *)
    07    solve_mets : References_Def.id list,(* methods solving the T          *)
    08    where_rls : Rule_Set.T,             (* for evaluation of preconditions*)
    09    where_ : Pre_Conds.unchecked,       (* preconditions as terms         *)
    10    model : Model_Pattern.T             (* "#Given", "#Find", "#Relate"   *)
    11  }

By this type problems are stored in a tree borrowed from Isabelle; the key
["univariate_calculus", Optimisation""] into this tree is created from the
string "univariate_calculus/Optimisation" in Fig.5:

      01  type store = (T Store.node) list

###  4.5 Efficiency Considerations with Parsing

Two decades ago, at the time when ISAC started with development, parsing
required substantial resources. Thus a specific component, O_Model.T was
shifted in-between Formalise.model (p.3.2) and the interaction model I_Model.T
(p.4.2).

    01  type O_Model.single =
    02    variants *     (* pointers to variants given in Formalise.T *)
    03    m_field *      (* #Given | #Find | #Relate                  *)
    04    descriptor *   (* see Input_Descript.thy                    *)
    05    values         (* HOLlist_to_MLlist t | [t]                 *)
    06    );
    07  type O_Model.T = O_Model.single list;

This structure is created at the beginning of the specify-phase (by
Tactic.Model_Problem). The terms are already parsed, descriptor and values
conveniently separated; also the variants are ready for convenient handling.
At the occasion of parsing also an Isabelle Proof_Context is fed with the
types of all variables in Formalise.model. This discharges the student of the
necessity to explicitly input types.

#### Refinement of types of equations

as introduced by UR.12 is particularly resources consuming: Fig.3 on p.3 shows
that already the old prototype implemented quite a lot of types of equations.
Refinement starts at the root ["univariate", "equation"] of the branch, an
environment with respect to the given equation has to be created from the
I_Model.T and the current Model_Pattern.T, with this environment for each node
in the tree the respective "#Given" and "#Where" needs to be instantiated, and
last not least the latter requires evaluation by rewriting (see §4.6 below).

All that tasks act on terms, i.e. require parsing. If this is done during
interactive problem solving, response time will get to high even with modern
hardware. Thus not only Problem.T (see definition on p.3.2) contains terms
alreay parsed, but also Model_Pattern.T and other structures. These structures
(Model_Pattern.T, Problem.T, MethodC.T and Error_Pattern.T) hold terms, where
the exact type is not known at compile time, and where the type needs to be
adapted to the current Problem.T. Thus all these structures have a function

    01  val adapt_to_type Proof.context -> T -> T

and these functions in turn call

    01  val adapt_term_to_type: Proof.context -> term -> term

which is defined in structure ParseC.

###  4.6 Pre-Conditions in Problems and Methods

Pre-conditions are an essential part of a formal specification (definition in
§2.2 Pt.2 on p.2). We compare the definition to ISAC’s representation of a
Model (e.g. on p.1, p.2 or p.4):

formal specification |  ISAC’s Model
---|---
$\it{in}$ | Given
$\it{Pre}\;(\it{in})$ | Where
$\it{out}$ | Find
$\it{Post}\;(\it{in},\,\it{out})$ | Relate

However, type Model_Pattern.T (defintion on p.3.2) does _not_ contain a
precondition ($\it{Pre}\;(\it{in})$, Where) and so does the actual Model of a
Problem.T (defintion on p.4.4; for specifics of Relate see p.3.3). The reason
is that the role of items in a Model is to conform with a particular
Formalise.model (made ready by parsing in I_Model.T) and whether it is present
or not – whereas a precondition must evaluate to true in order to make a Model
complete; this involves rewriting. The implementation details are as follows.

    01  type Pre_Conds.T = (bool * term) list;
    02  type Pre_Conds.unchecked_pos = (term * Position.T) list
    03  type Pre_Conds.checked_pos = bool * ((bool * (term * Position.T)) list)

The role of preconditions is different from Model-items such that
preconditions are stored only in a Problem.T (accompanied by a Model) and
evaluated by use of environments, which are generated on the fly according to
I_Model actually input:

    01  val make_environments: Model_Pattern.T -> I_Model.T ->
    02    Env.T * (env_subst * env_eval)
    03  val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos ->
    04    Model_Pattern.T * I_Model.T -> checked_pos

##  5 Summary and Conclusions

This is the first concise description of how the ISAC prototype models the
specify-phase. The specify-phase concerns the transition from a problem
statement given in the form prose text and/or illustrations to a formal
specification.

The description starts with user requirements in §2 and thus presents the
perspective of students solving exercises in engineering studies (similar
learning scenarios can be found in secondary schools). Here is also the
definition of the notion “formal specification” as given by input and output
as well as precondition and postcondition. §3 describes the design of the
specify-phase with regard to the user requirements and identifies open design
issues. The description of the implementation in §4 emphasises the generic
tools of Isabelle/Isar and the powerful helper functions of Isabelle/ML to
motivate readers to use existing proof assistants as a basis for the
development of for the development of learning systems rather than starting
from scratch again and again.

Another motivation for this description is to inform future collaborators of
the Isac project about implementation details and its background.

#### Conclusions

Over the decades, Isac’s design of the specify-phase and the solve-phase was
discussed long and wide and has proven useful in field tests; the time is ripe
to move into development for widespread use. It seems helpful that the old
Java-based front end has been abandoned and that the originally very ambitious
specifications [21] are significantly reduced: ISAC will change from a multi-
user system to a single-user system in line with the (current) architecture of
Isabelle/PIDE; and in the next step of development the scope of application
will be limited to inclusive learning situations (visually impaired students
integrated) in secondary educational institutions to take advantage of the
structural relationship between Isabelle’s terms and the Braille display.

The sudden penetration of AI will pose the following new research tasks.
Starting from a differentiation of problem solving through

  1. 1.

intuitively and associatively thinking humans (who bear responsibility for
their actions, etc)

  2. 2.

AI with deep learning

  3. 3.

formal mathematics

the interaction of (3) and (2) will be analysed. Design and implementation of
a user guide and a user model (from the interaction of (3) and (1)) is already
planned in the next development step.

## References

  * [1]
  * [2] Ralph-Johan Back & Joakim von Wright (1998): _Refinement Calculus: A Systematic Introduction_.  Springer-Verlag.  Graduate Texts in Computer Science, 10.1007/978-1-4612-1674-2.
  * [3] Christoph Benzmüller & David Fuenmayor (2021): _Value-Oriented Legal Argumentation in Isabelle/HOL_.  In Liron Cohen & Cezary Kaliszyk, editors: 12th International Conference on Interactive Theorem Proving (ITP 2021), Leibniz International Proceedings in Informatics (LIPIcs) 193, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 7:1–7:20, 10.4230/LIPIcs.ITP.2021.7.
  * [4] Bruno Buchberger (2023): _Is ChatGPT Smarter Than Master’s Applicants?_ RISC Report Series 23-04, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria.  Available at https://www3.risc.jku.at/publications/download/risc_6684/23-04.pdf.
  * [5] Jasmin C.Blanchette: _Hammering Away. A User’s Guide to Sledgehammer for Isabelle/HOL_.  contained in the Isabelle distribution.  Available at http://isabelle.in.tum.de/doc/sledgehammer.pdf.
  * [6] Gabriella Daróczy & Walther Neuper (2013): _Error-Patterns within “Next-Step-Guidance” in TP-based Educational Systems_.  In: eJMT, the Electronic Journal of Mathematics & Technology, 7, pp. 175–194.  Available at https://php.radford.edu/~ejmt/ContentIndex.php#v7n2.  Special Issue “TP-based Systems and Education”.
  * [7] Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz & Makarius Wenzel (2021): _The Isabelle/Naproche natural language proof assistant (system description)_.  In: 28th International Conference on Automated Deduction (CADE 28), Lecture Notes in Computer Science, Springer-Verlag, 10.1007/978-3-030-79876-5_36
  * [8] Karl Josef Fuchs, Simon Plangg, Martin Stein & Gilbert Greefrath, editors (2020): _Computer Algebra Systeme in der Lehrer(innen)bildung (überarbeitete Neuauflage)_.  WTM Verlag, Münster.
  * [9] David Gries (1981): _The science of programming_.  Texts and monographs in computer science, Springer-Verlag, 10.1007/978-1-4612-5983-1.
  * [10] Mateja Jamnik (2023): _How Can We Make Trustworthy AI?_ In Marco Gaboardi & Femke van Raamsdonk, editors: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Leibniz International Proceedings in Informatics (LIPIcs) 260, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 2:1–2:1, 10.4230/LIPIcs.FSCD.2023.2.
  * [11] Franz Kober (2012): _Logging of High-Level Steps in a Mechanized Math Assistant_.  Master’s thesis, IICM, Graz University of Technology.  https://static.miraheze.org/isacwiki/e/e6/Fkober_bakk.pdf.
  * [12] Klaus Miesenberger, Walther Neuper, Bernhard Stöger & Makarius Wenzel (2023): _Towards an Accessible Mathematics Working Environment Based on Isabelle/VSCode_.  In Pedro Quaresma, João Marcos & Walther Neuper, editors: Proceedings 11th International Workshop on Theorem Proving Components for Educational Software, Haifa, Israel, 11 August 2022, Electronic Proceedings in Theoretical Computer Science 375, Open Publishing Association, pp. 92–111, 10.4204/EPTCS.375.8.
  * [13] Robin Milner, Mads Tofte, Robert Harper & David MacQueen (1997): _The Definition of Standard ML (Revised)_.  The MIT Press, Cambridge, London, 10.7551/mitpress/2319.001.0001.
  * [14] Walther Neuper (2012): _Automated Generation of User Guidance by Combining Computation and Deduction_.  In Pedro Quaresma & Ralph-Johan Back, editors: Electronic Proceedings in Theoretical Computer Science, 79, Open Publishing Association, pp. 82–101, 10.4204/EPTCS.79.5.
  * [15] Walther Neuper (2019): _Technologies for “Complete, Transparent & Interactive Models of Math” in Education_.  In Pedro Quaresma & Walther Neuper, editors: Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 july 2018, Electronic Proceedings in Theoretical Computer Science 290, Open Publishing Association, pp. 76–95, 10.4204/EPTCS.290.6.
  * [16] Walther Neuper (2020): _Lucas-Interpretation on Isabelle’s Functions_.  In Pedro Quaresma, Walther Neuper & João Marcos, editors: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software (ThEdu’20), Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science, 328, pp. 79–95, 10.4204/EPTCS.328.5.
  * [17] Walther Neuper & Christian Dürnsteiner (2007): _Angewandte Mathematik und Fachtheorie mithilfe adaptierter Basis-Software_.  Technical Report 683, IMST – Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.  Available at https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf.
  * [18] Walther Neuper, Johannes Reitinger & Angelika Gründlinger (2008): _Begreifen und Mechanisieren beim Algebra Einstieg_.  Technical Report 1063, IMST – Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.  Available at https://www.imst.ac.at/imst-wiki/images/9/9d/1063_Langfassung_Reitinger.pdf.
  * [19] Walther Neuper et al. (2006): _Angewandte Mathematik und Fachtheorie_.  Technical Report 357, IMST – Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.  Available at http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte_Mathematik_und_Fachtheorie.
  * [20] Lawrence C. Paulson, Tobias Nipkow & Makarius Wenzel (2019): _From LCF to Isabelle/HOL_.  Formal Aspects of Computing 31, pp. 675–698,  Springer, London, 10.1007/s00165-019-00492-1.
  * [21] ISAC Team (2002): _ISAC – User Requirements Document, Software Requirements Document, Architectural Design Document, Software Design Document, Use Cases, Test Cases_.  Technical Report, Institute for Softwaretechnology, University of Technology.  Available at https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf.
  * [22] Makarius Wenzel & Burkhart Wolff (2011): _Isabelle/PIDE as Platform for Educational Tools_.  In Pedro Quaresma & Ralph-Johan Back, editors: Proceedings First Workshop on CTP Components for Educational Software, THedu’11, Wroclaw, Poland, 31th July 2011, EPTCS 79, pp. 143–153, 10.4204/EPTCS.79.9.
  * [23] Markus Wenzel (1999): _Isar - a Generic Interpretative Approach to Readable Formal Proof Documents_.  In G. Dowek, A. Hirschowitz, C. Paulin & L. Thery, editors: Theorem Proving in Higher Order Logics, LNCS 1690, 12th International Conference TPHOLs’99, Springer, 10.1007/3-540-48256-3_12.
  * [24] W.Neuper, B.Stöger & M.Wenzel (2022): _Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode_.  Isabelle Workshop 2022 https://sketis.net/isabelle/isabelle-workshop-2022.  Accessed: 202-10-13.