# Internal Heating in Magnetars: Role of Electron Captures

Nicolas Chamel1, Anthea Francesca Fantina 2,1 Lami Suleiman 3,4 Julian-Leszek
Zdunik 3 and Pawel Haensel 3 1Institute of Astronomy and Astrophysics,
Université Libre de Bruxelles, CP 226, Boulevard du Triomphe, B-1050 Brussels,
Belgium
2Grand Accélérateur National d’Ions Lourds (GANIL), CEA/DRF-CNRS/IN2P3,
Boulevard Henri Becquerel, 14076 Caen, France
3N. Copernicus Astronomical Center, Polish Academy of Sciences, Bartycka 18,
PL-00-716 Warszawa, Poland
4Laboratoire Univers et Théories, Observatoire de Paris, CNRS, Université
Paris Cité, 92195 Meudon, France<EMAIL_ADDRESS>
###### Abstract

The role of electron captures by nuclei in the shallow heating of magnetars is
further investigated using both nuclear measurements and the theoretical
atomic mass table HFB-27. Starting from the composition of the outer crust in
full equilibrium, we have calculated the onset of electron captures and the
heat released due to the slow decay of the magnetic field. Numerical results
are found to be similar to those previously obtained with the HFB-24 atomic
mass model and are consistent with neutron-star cooling data.

##  1 Introduction

With their extreme magnetic fields, soft gamma-ray repeaters and anomalous
X-ray pulsars are very active types of neutron stars exhibiting outbursts and
more rarely giant flares releasing energies up to $\sim 10^{46}$ erg within a
second (see e.g. [1] for a recent review). So far, 24 of these magnetars have
been identified according to the McGill Online Magnetar
Catalog111http://www.physics.mcgill.ca/~pulsar/magnetar/main.html [2]. Their
magnetic field is also thought to power their persistent X-ray luminosity
$\sim 10^{33}-10^{35}$ erg/s, which is well in excess of their rotational
energy and which implies higher surface temperatures than in weakly magnetized
neutron stars of the same age [3]. The most widely accepted heating mechanism
involves crustal deformations beyond the elastic limit induced by magnetic
stresses (see, e.g., Ref. [4]; see Ref. [5] for alternative models). Because
the melting temperature of an electron-ion Coulomb solid increases with
density [6, 7], this mechanism is most effective in the inner region of the
crust. However, heat sources are not expected to be found in such deep region
of the star [8, 9].

Alternatively, the magnetic energy may be converted into heat through electron
captures by nuclei in the outer crust [10]. This mechanism is analogous to
crustal heating in accreting neutron stars [11], the matter compression being
induced here by the magnetic-field decay rather than accretion from a stellar
companion. We have recently estimated the maximum amount of heat that could be
possibly released by these processes and the location of the heat sources
[12]. In addition to electron captures, we have also considered pycnonuclear
fusion of light elements. After briefly reviewing our assumptions and our
treatment of dense matter, new results are reported using a different nuclear
model.

##  2 Compression-induced reactions in magnetar crusts

###  2.1 Initial composition

We assume that each crustal layer is made of nuclei $(A,Z)$ with proton number
$Z$ and mass number $A$ in a charge neutralizing background of free electrons.

We take into account Landau-Rabi quantization for electrons (see, e.g. Chapter
4 of Ref. [13]) and consider that electrons all lie in the lowest level, which
occurs whenever $B\gtrsim 5.72\times 10^{16}$ G [14]. Quantization effects are
expected to be very strong for such fields because the temperatures prevailing
in a magnetar, $T\sim 10^{8}-10^{9}$ K, are much lower than the characteristic
temperature

$T_{B}=\frac{m_{e}c^{2}}{k_{B}}B_{\star}\approx 5.93\times
10^{9}B_{\star}~{}\rm K\,,$ (1)

where $k_{B}$ denotes Boltzmann’s constant, $c$ is the speed of light, $m_{e}$
is the electron mass, and we have introduced the dimensionless magnetic field
strength $B_{\star}\equiv B/B_{\rm rel}\gg 1$ with:

$B_{\rm rel}=\frac{m_{e}^{2}c^{3}}{e\hbar}\approx 4.41\times 10^{13}\,\rm
G\,,$ (2)

($e$ is the elementary electric charge and $\hbar$ is the Planck-Dirac
constant).

The electron-ion plasma may not necessarily be in a solid state, especially in
the shallow layers. A lower bound on the melting temperature can be found by
ignoring the magnetic field [15], and is typically of order $T_{m}\sim 10^{9}$
K (see Ref. [6] for more details).

In this study, thermal effects on thermodynamic quantities will be neglected.

Assuming the crust is initially in full thermodynamic equilibrium in presence
of some magnetic field, the composition is found by minimizing the Gibbs free
energy per nucleon (see Ref. [16]). This minimization can be performed
numerically in a very efficient way by using the iterative approach proposed
in Ref. [17].

###  2.2 Magnetic field decay and electron captures

The compression of the crust induced by the decay of the magnetic field occurs
very slowly, on a typical time scale of millions of years [18]. The capture of
one electron by the nucleus $(A,Z)$ (in its ground state since matter is
assumed to be initially in equilibrium) becomes allowed once the local
pressure attains some threshold value $P_{\beta}(A,Z,B_{\star})$, which can be
calculated analytically and is given by [12]

$\displaystyle P_{\beta}(A,Z,B_{\star})$ $\displaystyle\approx$
$\displaystyle\frac{B_{\star}m_{e}c^{2}}{4\pi^{2}\lambda_{e}^{3}}\biggl{[}\gamma_{e}\sqrt{\gamma_{e}^{2}-1}-\ln\left(\sqrt{\gamma_{e}^{2}-1}+\gamma_{e}\right)$
(3)
$\displaystyle+\frac{C\alpha}{3}\left(\frac{4B_{\star}Z^{2}}{\pi^{2}}\right)^{1/3}\left(\gamma_{e}^{2}-1\right)^{2/3}\biggr{]}\,,$

where $\lambda_{e}=\hbar/(m_{e}c)$ is the electron Compton wavelength,
$\alpha=e^{2}/(\hbar c)$ is the fine-structure constant, $C$ is a
dimensionless constant characterizing the spatial arrangements of nuclei and
for which we adopt the Wigner-Seitz value
$C=-9/10(4\pi/3)^{1/3}\approx-1.4508$ [19]. Here $\gamma_{e}$ is the threshold
electron Fermi energy in units of $m_{e}c^{2}$ given by [12]

$\gamma_{e}=\left\\{\begin{array}[]{ll}\displaystyle
8|\bar{F}(Z,B_{\star})|^{3/2}\,{\rm cosh}^{3}\left(\frac{1}{3}{\rm
arccosh~{}}\frac{\gamma_{e}^{\beta}}{2|\bar{F}(Z,B_{\star})|^{3/2}}\right)&{\rm
if}\ \upsilon\geq 1\,,\\\ \displaystyle
8|\bar{F}(Z,B_{\star})|^{3/2}\,\cos^{3}\left(\frac{1}{3}\arccos\frac{\gamma_{e}^{\beta}}{2|\bar{F}(Z,B_{\star})|^{3/2}}\right)&{\rm
if}\ 0\leq\upsilon<1\,,\end{array}\right.$ (4)

with

$\bar{F}(Z,B_{\star})\equiv\frac{1}{3}C\alpha\left(\frac{B_{\star}}{2\pi^{2}}\right)^{1/3}\biggl{[}Z^{5/3}-(Z-1)^{5/3}+\frac{1}{3}Z^{2/3}\biggr{]}\,,$
(5) $\gamma_{e}^{\beta}\equiv-\frac{Q_{\rm EC}}{m_{e}c^{2}}+1\,,$ (6) $Q_{\rm
EC}(A,Z)=M^{\prime}(A,Z)c^{2}-M^{\prime}(A,Z-1)c^{2}-E_{\rm ex}(A,Z-1)\,.$ (7)

Here $M^{\prime}(A,Z)$ denotes the nuclear mass including the rest mass of $Z$
electrons and $E_{\rm ex}(A,Z-1)$ is the excitation energy of the daughter
nuclei. The mean baryon number density at the onset of the first electron
capture is given by [12]

$n_{\beta}(A,Z,B_{\star})=\frac{B_{\star}}{2\pi^{2}\lambda_{e}^{3}}\frac{A}{Z}\sqrt{\gamma_{e}^{2}-1}\,.$
(8)

No heat is released by this first electron capture since it proceeds in
quasiequilibrium. However, the daughter nucleus (in some excited state)
$(A,Z-1)$ is almost always unstable against a second electron capture off-
equilibrium thus depositing some heat at the _same_ pressure
$P_{\beta}(A,Z,B_{\star})$. The maximum amount of heat per nucleus can be
estimated analytically ignoring the fraction of energy carried away by
neutrinos [12]

$\displaystyle\mathcal{Q}(A,Z,B_{\star})$ $\displaystyle=$ $\displaystyle
Q_{\rm EC}(A,Z-1)-Q_{\rm EC}(A,Z)+2E_{\rm ex}(A,Z-1)$ (9) $\displaystyle-$
$\displaystyle
m_{e}c^{2}C\alpha\left(\frac{B_{\star}}{2\pi^{2}}\right)^{1/3}(\gamma_{e}^{2}-1)^{1/6}\biggl{[}Z^{5/3}+(Z-2)^{5/3}-2(Z-1)^{5/3}\biggr{]}\,.$

Leaving aside the small terms on the second line, the maximum heat released is
thus completely determined by nuclear data alone, independently of the
magnetic field and whether the electron-ion plasma is solid or not.

In the densest regions of the outer crust, fusion of the lightest nuclei might
occur [20]. Considering that such reactions become allowed at pressure $P_{\rm
pyc}=P_{\beta}$ yields the following upper bound on the heat released per
parent nucleus:

$\displaystyle\mathcal{Q}_{\rm pyc}(A,Z,B_{\star})$ $\displaystyle=$
$\displaystyle
M^{\prime}(A,Z-1)c^{2}-\frac{M^{\prime}(2A,2Z-2)c^{2}}{2}+E_{\rm ex}(A,Z-1)$
(10) $\displaystyle+$ $\displaystyle
m_{e}c^{2}C\alpha(1-2^{2/3})\left(\frac{B_{\star}\gamma_{e}}{2\pi^{2}}\right)^{1/3}(Z-1)^{5/3}\,,$

with $\gamma_{e}$ given by Eq. (4).

The bottom of the outer crust is marked by the emission of free neutrons [14,
21]. We have not considered reactions occurring in deeper layers (inner
crust).

##  3 Results and discussion

###  3.1 Numerical estimates

We have calculated the crustal heat using nuclear masses and
$Q_{\beta}(A,Z-1)=-Q_{\rm EC}(A,Z)$ values from the 2016 Atomic Mass
Evaluation [22], excitation energies from the Nuclear Data section of the
International Atomic Energy Agency website222https://www-
nds.iaea.org/relnsd/NdsEnsdf/QueryForm.html, as well as predictions from the
atomic mass model HFB-27 based on self-consistent deformed Hartree-Fock-
Bogoliubov calculations [23]. Further details can be found in Ref. [12]. The
magnetic field strength was set to $B_{\star}=2000$. The initial equilibrium
composition was taken from Ref. [17]. As for possible contamination of the
crust with light elements from the interstellar medium, we considered carbon
and oxygen. Results are summarized in Fig. 1.

Comparing the present results with those previously obtained using the HFB-24
mass model in Ref. [12], we notice that the reactions releasing the largest
amount of heat are the same, namely,
${}^{12}\mathrm{C}\rightarrow{}^{12}\mathrm{Be}$,
${}^{16}\mathrm{O}\rightarrow{}^{16}\mathrm{C}$, and
${}^{62}\mathrm{Cr}\rightarrow{}^{62}\mathrm{Ti}$ considering ground-state-to-
ground-state transitions (the heat released being $\sim 0.14$ MeV, $\sim 0.15$
MeV, and $\sim 0.09$ MeV per nucleon), and
${}^{82}\mathrm{Ge}\rightarrow{}^{82}\mathrm{Zn}$,
${}^{88}\mathrm{Sr}\rightarrow{}^{88}\mathrm{Kr}$,
${}^{88}\mathrm{Kr}\rightarrow^{88}\mathrm{Se}$, and
${}^{86}\mathrm{Kr}\rightarrow{}^{86}\mathrm{Se}$ considering ground-state-to-
excited-state transitions (the heat released being $\sim 0.1$ MeV, $\sim 0.08$
MeV, $\sim 0.07$ MeV, $\sim 0.09$ MeV per nucleon, respectively). Note that
for the latter reactions, as well as for the reactions involving carbon and
oxygen, the amount of heat released is only determined by experimental data,
thus independent of the adopted mass model (see also Tables 1 and 3 in Ref.
[12]). The most noticeable difference between the predictions of the mass
models HFB-24 and HFB-27 concerns the heat released in the ground-state-to-
ground-state transitions ${}^{56}\mathrm{Ti}\rightarrow{}^{56}\mathrm{Ca}$ and
${}^{80}\mathrm{Zn}\rightarrow{}^{80}\mathrm{Ni}$. In the former (latter)
reaction, the heat predicted by HFB-27 is a factor of $\sim 2$ ($\sim 3$)
higher than that calculated using the HFB-24 mass model. The reason stems from
the discrepancy in the $Q_{\rm EC}$ values, see Eq. (9). Indeed, the
difference in $|Q_{\rm EC}(Z)-Q_{\rm EC}(Z-1)|$ calculated using the HFB-24
and HFB-27 mass model amounts to $\sim 1.3$ MeV ($\sim 0.9$ MeV) for the
transition from ${}^{56}\mathrm{Ti}$ to ${}^{56}\mathrm{Ca}$ (from
${}^{80}\mathrm{Zn}$ to ${}^{80}\mathrm{Ni}$).

Figure 1: Heat $q$ per nucleon (in MeV) from selected electron captures in the
crust of a magnetar with a magnetic field $B_{\star}=2000$ in a pressure $P$
(in dyn cm-2)–mass density $\rho$ (in g cm-3) diagram, considering transitions
from the ground state of the parent nucleus to either the ground state
(squares) or the first excited state (triangles) of the daughter nucleus. The
size of each symbol is proportional to the amount of heat deposited as
indicated.

The maximum amount of heat released per nucleon is found to be $\sim 0.1$ MeV
from electron captures, and $\sim 1-2$ MeV from pycnonuclear fusions. The
total amount of heat deposited in the outer crust of a magnetar is comparable
to that found in accreting neutron stars although the initial composition and
the physical conditions are totally different [25]. However, heat in a
magnetar is deposited at higher densities, $\rho_{\beta}\sim 10^{10}-10^{11}$
g cm-3 (corresponding to pressures $P_{\beta}\sim 10^{29}-10^{30}$ dyn cm-2)
for the magnetic field considered.

###  3.2 Astrophysical implications

The range of densities where most of the heat from nuclear reactions is
released corresponds to that determined empirically by fitting the observed
thermal luminosity using magnetar cooling simulations [8, 9].

The time $\tau$ required for all the nuclei $(A,Z)$ to capture electrons,
roughly given by [12]

$\tau\sim\frac{4\pi}{B^{2}}\biggl{[}P_{\beta}(A,Z,B_{\star})-P_{\rm
min}(A,Z,B_{\star})\biggr{]}~{}\rm Myr$ (11)

($P_{\rm min}(A,Z,B_{\star})$ being the lowest pressure at which parent nuclei
$(A,Z)$ were initially found), is of the same order in the different crustal
layers, and more importantly of the same order as the kinematic age of
magnetars (a few thousand years).

Finally, the heat power, estimated as [12]

$W^{\infty}\sim\frac{1}{\tau}\sum\mathcal{Q}(A,Z)\mathcal{N}(A,Z)\sim
10^{35}-10^{36}\ \rm erg/s\,,$ (12)

where $\mathcal{N}(A,Z)$ is the total number of nuclei $(A,Z)$, is of the same
order as that obtained in Refs. [8, 9].

The compression of matter caused by the spin down of the star could also
trigger nuclear reactions, as studied in millisecond pulsars [26]. However,
this heating becomes ineffective several days after the formation of the star
[12] and can thus be ignored.

##  4 Conclusions

Our analysis suggests that electron captures by nuclei and pycnonuclear fusion
reactions in the outer crust of a magnetar induced by the decay of the
magnetic field could be a robust source of internal heating. Unlike the
commonly accepted dissipation of elastic energy due to crust failure, the
heating from electron captures remains effective even if some part of the
crust is melted. Although for simplicity we have considered an extremely
quantizing magnetic field, we have shown that the maximum amount of heat is
essentially determined by nuclear data alone. Therefore, our estimate remains
a fairly good approximation for neutron stars with lower magnetic fields, as
confirmed by our recent study [27]. Only the location of the heat sources will
vary substantially depending on the magnetic field strength. The models HFB-24
and HFB-27 predict similar results for the main heat sources, however
significant differences are found for some minor reactions.

The work of N.C. was funded by Fonds de la Recherche Scientifique-FNRS
(Belgium) under Grant Number IISN 4.4502.19. L.S., P.H., and J-L.Z.
acknowledge the financial support from the National Science Centre (Poland)
Grant Number 2018/29/B/ST9/02013. This work was also partially supported by
the European Cooperation in Science and Technology Action CA16214 and the CNRS
International Research Project (IRP) “Origine des éléments lourds dans
l’univers: Astres Compacts et Nucléosynthèse (ACNu)”.

## References

## References

  * [1] Esposito, P., Rea, N., Israel, G.L. 2021, in: T.M. Belloni, M. Méndez & C. Zhang (eds.), Astrophysics and Space Science Library (Springer, Berlin/Heidelberg, Germany), p. 97
  * [2] Olausen, S. A. & Kaspi, V. M. 2014, ApJS, 212, 6
  * [3] Vigano, D., Rea, N., Pons, J. A., Perna, R., Aguilera, D. N., Miralles, J. A. 2013, MNRAS, 434, 123
  * [4] De Grandis, D., Turolla, R., Wood, T.S., Zane, S., Taverna, R., & Gourgouliatos, K.N. 2020, ApJ 903, 40
  * [5] Beloborodov, A.M. & Li, X. 2016, ApJ, 833, 261
  * [6] Fantina, A. F., De Ridder, S., Chamel, N., Gulminelli, F. 2020, A&A, 633, A149
  * [7] Carreau, T., Gulminelli, F., Chamel, N., Fantina, A. F., Pearson, J. M. 2020, A&A, 635, A84
  * [8] Kaminker, A.D., Yakovlev, D.G., Potekhin, A.Y., Shibazaki, N., Shternin, P.S., & Gnedin, O.Y. 2006, MNRAS, 371, 477
  * [9] Kaminker, A.D., Potekhin, A.Y., Yakovlev, D.G., & Chabrier, G. 2009, MNRAS, 395, 2257
  * [10] Cooper, R.L., Kaplan, D.L. 2010, ApJ (Letters), 708, L80
  * [11] Haensel, P., & Zdunik, J. L. 1990, A&A, 227, 431
  * [12] Chamel, N., Fantina, A.F., Suleiman, L., Zdunik, J.-L. & Haensel, P. 2021, Universe, 7(6), 193
  * [13] Haensel, P., Potekhin, A. Y., & Yakovlev, D. G. 2007, Neutron Stars 1. Equation of State and Structure (New York, Springer, 2007)
  * [14] Chamel, N., Stoyanov, Z.K., Mihailov, L.M., Mutafchieva, Y.D., Pavlov, R.L., Velchev, C.J. 2015, Phys. Rev. C, 91, 065801
  * [15] Potekhin, A.Y., Chabrier, G. 2013, A&A, 550, A43
  * [16] Chamel, N., Fantina, A.F. 2015, Phys. Rev. D, 92, 023008
  * [17] Chamel, N., & Stoyanov, Zh. K. 2020, Phys. Rev. C, 101, 065802 (2020)
  * [18] Pons, J.A., Viganò, D. 2019, Living Rev. Comput. Astrophys. 5, 3
  * [19] Salpeter, E.E. 1954, Aust. J. Phys., 7, 373
  * [20] Yakovlev, D. G., Gasques, L. R., & Wiescher, M. 2006, MNRAS, 371, 1322
  * [21] Chamel, N., Fantina, A.F., Zdunik, J.L., & Haensel, P. 2015, Phys. Rev. C, 91, 055803
  * [22] Wang, M., Audi, G., Kondev, F.G., Huang, W.J., Naimi, S., & Xu, X. 2017, Chin. Phys. C, 41, 030003
  * [23] Goriely, S., Chamel, N., Pearson, J. M. 2013, Phys. Rev. C, 88, 061302
  * [24] Lunney, D., Pearson, J. M., & Thibault, C. 2003, Rev. Mod. Phys., 75, 1021
  * [25] Chamel, N., Fantina, A.F., Zdunik, J.-L., Haensel, P. 2020, Phys. Rev. C, 102, 015804
  * [26] Iida, K. & Sato, K. 1997, ApJ, 477, 294
  * [27] Chamel, N., Fantina, A.F. 2022, Universe, 8(6), 328


remarkRemark hypothesisHypothesis claimClaim Random variable transformed by
Chebyshev PolynomialsJavier Chico Vázquez, Andrew J. Horning ex_supplement

# The limiting distribution of a random variable transformed by Chebyshev
Polynomials

Javier Chico Vázquez Imperial College LondonMathematical Institute, University
of Oxford Andrew J. Horning Massachusetts Institute of Technology

###### Abstract

In this paper we present the result of successively applying a Chebyshev
polynomial to a continuous random variable. In particular we show that under
mild assumptions the limiting distribution will be the same as the weight with
respect to which Chebyshev polynomials are orthogonal, namely
$\sim(1-t^{2})^{-\frac{1}{2}}$.

###### keywords:

Chebyshev polynomials, Convergence in distribution

##  1 Introduction

This paper investigates the behaviour of a random variable $X$ when it is
transformed by Chebyshev polynomials. Mathematically, we are interested in the
distribution of $T_{k}(X)$, in particular on how this behaves as
$k\rightarrow\infty$. In particular, we will show that this converges in
distribution to a continuous random variable whose density function is the
same as the weight function under which Chebyshev polynomials are orthogonal.
Further, we show that the limiting distribution is invariant when transformed
by $T_{k}$.

The structure of this paper is the following: First we review necessary
concepts in Section 2. Next we state the main result in Section 3, with an
interesting asymptotic analysis of the error and the statement for a lemma
which serves as a cornerstone for the proof. This is followed by a
presentation of the numerical results. In the next section a rigorous proof
for the theorem is presented, and the final remarks include results that seem
to hold from the numerics but have not been shown formally.. In the final
appendix the proof for the lemma is presented.

##  2 Preliminaries

We introduce some important definitions and results before presenting the main
results. First, for convenience, we define the $k^{th}$ Chebyshev polynomial
of the first kind as [7, 1, 4]

(1) $T_{k}(x)=\cos(k\cos^{-1}(x))$

where $\cos^{-1}=\arccos{}$. Chebyshev polynomials are orthogonal in the
following sense: [1]

(2) $\int_{-1}^{1}T_{k}(x)T_{l}(x)w(x)\text{d}x=0\text{ when }k\neq l\text{
and }w(x)=\frac{1}{\sqrt{1-x^{2}}}$

The integral of a Chebyshev polynomial over $[-1,1]$ is given by [6]

(3)
$\int_{-1}^{1}T_{k}(x)\text{d}x=\begin{cases}\frac{(-1)^{k}+1}{1-k^{2}}&k\neq
1\\\ 0&k=1\end{cases}$

The following identities for the sums of cosines and sines will be useful
later. These are standard results from trigonometry [6].

(4a) $\displaystyle\sum_{j=1}^{n}\cos(jx)$
$\displaystyle=\frac{\sin(nx/2)\cos((n+1)x/2)}{\sin(x/2)}$ (4b)
$\displaystyle\sum_{j=1}^{n}\sin(jx)$
$\displaystyle=\frac{\sin(nx/2)\sin((n+1)x/2)}{\sin(x/2)}$

Once the above has been collected we can proceed by stating the main results
and the proof.

##  3 Main results

As mentioned previously, we are interested in the distribution of $T_{k}(X)$
as $k$ gets large. In particular, under mild assumptions, the following fact
holds: $T_{k}(X)$ will converge in distribution to a random variable whose
density function is the same as the weight function for Chebyshev polynomials.

######  Theorem 3.1.

Suppose $X$ is a continuous random variable with density function $f_{X}$ on
$[-1,1]$. As it is continuous, it can be expanded as a Chebyshev series that
converges absolutely [7, 5]

(5) $f_{X}(x)=\sum_{l=0}^{\infty}\mu_{l}T_{l}(x)$

then $T_{k}(X)$ converges in distribution to a random variable $\Gamma$ with
probability density function as $k\rightarrow\infty$

$f_{\Gamma}(z)=\frac{1}{\pi}\frac{1}{\sqrt{1-z^{2}}}$

This limiting random variable $\Gamma$ is a scaled and shifted Beta
distribution with parameters $\alpha=\beta=\frac{1}{2}$. In particular, if
$Y\sim\operatorname{Beta}(\alpha=\frac{1}{2},\beta=\frac{1}{2})$, then
$\Gamma=2Y-1$.

For a more general $X$ defined on $[a,b]$ we can re-scale the Chebyshev
polynomials on that interval, with a suitably re-defined weight function as
well. The theorem rests on the following result, which provides us with an
analytic formula for the probability density function of $T_{k}(X)$

######  Lemma 3.2.

Let $f_{X}$ and $F_{X}$ be the pdf and cdf of $X$, a continuous random
variable define on $[-1,1]$. Then the probability density function of
$T_{k}(X)$ when $k=2m$ is even is

(6)
$\begin{split}f_{k}(z)&=\frac{1}{\sqrt{1-z^{2}}}\sum_{j=1}^{m=\frac{k}{2}}\left\\{f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))\right\\}\\\
&=\frac{1}{\sqrt{1-z^{2}}}S_{k}(z)\end{split}$

where $S_{k}(z)$ is defined as the sum in the top line. When $k=2m+1$ is odd
there is an extra term in the sum

$\displaystyle f_{k}(z)=$
$\displaystyle\frac{1}{\sqrt{1-z^{2}}}\sum_{j=1}^{m=\frac{k-1}{2}}\\{f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))\\}$ $\displaystyle+$
$\displaystyle\frac{1}{\sqrt{1-z^{2}}}f_{\Psi_{k}}(2\pi m+\cos^{-1}(z))$

where $f_{\Psi_{k}}$ is the pdf of $\Psi_{k}=k\cos^{-1}(X)$, so that

$f_{\Psi_{k}}(\psi)=\frac{1}{k}f_{X}(\cos(\psi/k))\sin(\psi/k)$

###  3.1 Asymptotic analysis of the convergence

If we expand the expression for the complete sum in the general case, Eq. 11a,
around $k\rightarrow\infty$ we obtain the following expansion,

(8)
$\begin{split}S_{k}(z)&\approx\frac{1}{\pi}+\frac{1}{k^{2}}\left(\frac{\pi}{3}-\frac{(\pi-\cos^{-1}(z))^{2}}{\pi}\right)\left[\mu_{0}+\sum_{l=2}^{\infty}\left\\{\mu_{l}\cos\left(\frac{l\pi}{2}\right)^{2}\right\\}\right]+\mathcal{O}\left(\frac{1}{k^{4}}\right)\\\
&=\frac{1}{\pi}+\frac{1}{k^{2}}\left(\frac{\pi}{3}-\frac{(\pi-\cos^{-1}(z))^{2}}{\pi}\right)\sum_{l=0}^{\infty}\mu_{2l}+\mathcal{O}\left(\frac{1}{k^{4}}\right)\end{split}$

In particular, we see that the error is quadratic in $\frac{1}{k}$, thus
explaining the rapid convergence found numerically in the upcoming sections.
Furthermore, only the even Chebyshev moments contribute to the error.

##  4 Numerical Results

###  4.1 Dance around the origin

For distributions where the bulk of the probability mass is centered at the
origin (i.e. Gaussian, Cauchy, …), the second Chebyshev polynomial
$T_{2}(t)=2t^{2}-1$ will map most of that probability mass to $T_{2}(0)=-1$,
so the distribution will become skewed to the left. From there on, as
$T_{k}(1)=1$ and $T_{k}(-1)=(-1)^{k}$, the probability mass will remain mostly
on $t=-1$ for $k=3$, but will migrate to $t=1$ at $k=4$, and then oscillate
between $-1$ and $1$ changing place every two iterations, but loosing
skewedness as $k$ increases, as we know that the distribution eventually
converges to $\frac{1}{\pi\sqrt{1-t^{2}}}$ which is symmetric. This
oscillation is visualized in Fig. 1, where the initial distribution is a
Gaussian.

Figure 1: Dance around the origin for an initial Gaussian distribution. The
solid black lines represent the analytic solution as given by Lemma 3.2 and
the dashed red line represents the limiting distribution

In Fig. 1 we further observe that after only 24 iterations the distribution
has essentially converged (very quickly!), indeed, as we will see in the next
section this is because the convergence is quadratic in $\frac{1}{k}$, so that
the error decreases with $\mathcal{O}(\frac{1}{k^{2}})$.

##  5 Proofs for the main results

Before proving the general case we will show the proof for the case
$X\sim\Gamma$ (in this particular case, instead of convergence we will have
that the distribution is invariant, i.e. $\Gamma=T_{k}(\Gamma)$ in
distribution. For this it is necessary to obtain a general formula for the
probability density function of $T_{k}(X)$, denoted as $f_{k}(z)$. More
formally:

######  Theorem 5.1 (The invariant measure).

If $X\sim\operatorname{Beta}(1/2,1/2)$ then
$T_{k}(X)\sim\operatorname{Beta}(1/2,1/2)$. This means that the distribution
$\operatorname{Beta}(1/2,1/2)$ is invariant under the transformation
$T_{k}:[-1,1]\longrightarrow[-1,1]$

######  Proof 5.2.

In this case

$f_{X}(x)=\frac{1}{\pi\sqrt{1-x^{2}}}$

then

$f_{\Psi_{k}}(\psi)=f_{\Theta}(\psi/k)/k=\frac{1}{k}f_{X}(\cos(\psi/k))\sin(\psi/k)=\frac{\sin(\psi/k)}{\pi
k\sqrt{1-\cos^{2}(\psi/k)}}=\frac{1}{k\pi}$

So this is a Uniform distribution!! (which depends on $k$) Finally, as
$f_{\Psi_{k}}(\psi)$ is constant, the sum is really simple in the case $k$
even.

$f_{k}(z)=\frac{1}{\sqrt{1-z^{2}}}\sum_{j=1}^{m}f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))=$
$=\frac{1}{\sqrt{1-z^{2}}}\sum_{j=1}^{k/2}(\frac{1}{k\pi}+\frac{1}{k\pi})=\frac{2}{k\pi\sqrt{1-z^{2}}}\sum_{j=1}^{k/2}1=\frac{1}{\pi\sqrt{1-z^{2}}}$

For $k$ odd we will just have one extra term (but $k$ is one unit greater) so
the result is the same and we are done.

We can now turn our attention to the proof for the general statement. We will
do this by first exploring the constraint on the Chebyshev moments that arises
from normalisation, and we will use that to our advantage to show that the
limit in Eq. 15 is indeed $\frac{1}{\pi}$.

######  Proof 5.3 (General case).

We have that

$f_{X}(x)=\sum_{l=0}^{\infty}\mu_{l}T_{l}(x)$

But $f_{X}$ is a pdf so in particular it satisfies

$1=\int_{-1}^{1}f_{X}(x)dx=\sum_{l=0}^{\infty}\mu_{l}\int_{-1}^{1}T_{l}(x)dx$

We can use Eq. 3 so that the constraint becomes

(9) $1=2\mu_{0}+\sum_{l=2}^{\infty}\mu_{l}\frac{(-1)^{l}+1}{1-l^{2}}$

This will be useful later. We will now proceed as in the simpler cases, by
computing the limit in Eq. 15.

$f_{\Psi_{k}}(\psi)=\frac{\sin(\psi/k)}{k}f_{X}(\cos(\psi/k)=\frac{\sin(\psi/k)}{k}\sum_{l=0}^{\infty}\mu_{l}T_{l}(\cos(\psi/k))$

But $T_{l}(\cos(\psi/k))=\cos\left(\frac{l}{k}\psi\right)$ so that

$f_{\Psi_{k}}(\psi)=\frac{\sin(\psi/k)}{k}\sum_{l=0}^{\infty}\mu_{l}\cos(l\psi/k)$

If we focus on $k=2m$ even, then the limit is

$\displaystyle\sum_{j=1}^{k/2}$ $\displaystyle f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))=$ (10)
$\displaystyle=\frac{1}{k}\sum_{j=1}^{k/2}\sum_{l=0}^{\infty}$
$\displaystyle\mu_{l}\sin(x_{k}j-\beta_{k})\cos(l(x_{k}j-\beta_{k}))+\sin((x_{k}(j-1)+\beta_{k})\cos(l(x_{k}(j-1)+\beta_{k})$

defining $\beta_{k}=\cos^{-1}(z)$ as before and $x_{k}=\frac{2\pi}{k}$. We can
exchange the order of summation as the infinite series converges absolutely.

$\sum_{l=0}^{\infty}\mu_{l}\frac{1}{k}\sum_{j=1}^{k/2}\left\\{\sin(x_{k}j-\beta_{k})\cos(l(x_{k}j-\beta_{k}))+\sin(x_{k}(j-1)+\beta_{k})\cos(l(x_{k}(j-1)+\beta_{k}))\right\\}$

thus, we can focus by fixing $l$ and computing the limit of the inner sum as
$k$ gets large. We will do this for three separate cases: $l=0,l=1$ and $l\geq
2$. For $l=0$ the sum is simplified as the cosines have zero argument so
become factors of 1. Thus we have to consider

$\frac{1}{k}\sum_{j=1}^{k/2}\left\\{\sin(x_{k}j-\beta_{k})+\sin(x_{k}(j-1)+\beta_{k})\right\\}=\frac{2\cos\left(\frac{\pi-\cos^{-1}(z)}{k}\right)}{k\sin(\pi/k)}$

In the limit as $k\rightarrow\infty$ this becomes $\frac{2}{\pi}$. We can see
this because $\sin(\pi/k)\sim\frac{\pi}{k}$ and the cosine in the denominator
converges to 1 as the argument converges to zero.

Moving on to the case $l=1$ we can regroup the terms and obtain that the sum
(and thus the limit) is identically zero. The summand in this case can be
expressed as

$\displaystyle\sin(x_{k}j-\beta_{k})\cos(x_{k}j-\beta_{k})+\sin(x_{k}(j-1)+\beta_{k})\cos(x_{k}(j-1)+\beta_{k})=$
$\displaystyle=\cos\left(\frac{2(\pi-\cos^{-1}(z)}{k}\right)\sin\left(\frac{2\pi(2j-1)}{k}\right)$

So when we sum over $j$ the first term can be moved outside as a constant and
the second term, using the formula in Eq. 4b gives us 0.

Finally, for the case $l\geq 2$, the sum will give us

$\displaystyle\frac{\cos(l\pi/2)^{2}}{2k\sin(\pi/k(l+1))\sin(\pi/k(1-l))}[\sin((2\pi+(l-1)\cos^{-1}(z))/k)+$
$\displaystyle+\sin((2\pi
l+(1-l)\cos^{-1}(z))/k)+\sin((2\pi-(l+1)\cos^{-1}(z))/k)+$
$\displaystyle+\sin((-2\pi l+(l+1)\cos^{-1}(z))/k)]$

As all the sines have an argument that is divided by $k$, in the limit they
can be replaced by their argument. This means there is massive cancellation.
In particular, in the limit,

$\displaystyle\frac{k^{2}\cos(l\pi/2)^{2}}{2k\pi^{2}(1-l^{2})}[4\pi/k]=\frac{1}{\pi}\frac{1+\cos(l\pi)}{1-l^{2}}=\frac{1}{\pi}\frac{1+(-1)^{l}}{1-l^{2}}$

but this is precisely the result in Eq. 3 multiplied by $\frac{1}{\pi}$. Upon
assembling the different case we thus get that in the limit

$\frac{2}{\pi}\mu_{0}+0\cdot\mu_{1}+\sum_{l=2}^{\infty}\mu_{l}\frac{1}{\pi}\frac{1+(-1)^{l}}{1-l^{2}}=\frac{1}{\pi}\left[2\mu_{0}+\sum_{l=2}^{\infty}\mu_{l}\frac{1+(-1)^{l}}{1-l^{2}}\right]=\frac{1}{\pi}$

from the constraint in Eq. 9, so we are done.

Before, moving on, we can reassemble the sum before passing onto the limit,
for it will be useful later.

(11a) $\displaystyle
S_{k}(z)=\frac{2\cos\left(\frac{\pi-\cos^{-1}(z)}{k}\right)}{k\sin(\pi/k)}$
$\displaystyle+$ (11b)
$\displaystyle+\frac{\cos(l\pi/2)^{2}}{2k\sin(\pi/k(l+1))\sin(\pi/k(1-l))}[\sin((2\pi+(l-1)\cos^{-1}(z))/k)+$
(11c) $\displaystyle+\sin((2\pi
l+(1-l)\cos^{-1}(z))/k)+\sin((2\pi-(l+1)\cos^{-1}(z))/k)+$ (11d)
$\displaystyle+\sin((-2\pi l+(l+1)\cos^{-1}(z))/k)]$

##  6 Final Remarks

All in all we have shown the main fact for mild assumptions on $X$, in
particular that it has a Chebyshev Expansion. In particular, we showed that if
the initial distribution is the same as the limiting then it is conserved.
Furthermore, we have explored the oscillatory behaviour at the initial stages
of the convergence.

In the future it would be interesting to analytically study the convergence of
discontinuous distributions, such as

$f_{X}(x)=\begin{cases}1&0<x<1\\\ 0&\text{else}\end{cases}$

as our numerical testing strongly suggests the same result applies, as seen in
Fig. 2

Figure 2: Numerical evidence for the convergence for a discontinuous random
variable.

Furthermore, we would like to explore how this result can be used to
accelerate bayesian methods spectral methods like [3]

A second possible area for further research is connecting the results
presented herein with the theory of Koopman and Perron-Frobenius (Transfer)
operators [2]. The main theorem in this paper is the limit for a particular
transfer operator applied to the discrete dynamical system with governing
equation given by the 3-term recurrence relation for Chebyshev polynomials
[7]:

(12) $x_{k+1}=2x_{0}x_{k}-x_{k-1}$

where $x_{0}\in[-1,1]$ is the initial condition.

##  7 Appendix

A constructive proof of Lemma 3.2 is first given, as it is essential for the
proof of the main theorem.

######  Proof 7.1.

We want to compute

$T_{k}(X)=\cos(k\cos^{-1}(X))$

We can motivate computing this quantity in two steps. First, figuring out the
distribution of the ”inner” part, $k\cos^{-1}(X)$, and then transforming this
with the outer cosine. Thus, let $\Theta=\cos^{-1}(X)$. Then

$F_{\Theta}(\theta)=\Pr(\Theta\leq\theta)=\Pr(\cos^{-1}(X)\leq\theta)=\Pr(X\geq\cos(\theta))$

as the cosine is monotonically decreasing in arccosine [-1,1], so we change
the sign of the inequality. Then

$F_{\Theta}(\theta)=1-\Pr(X\leq\cos(\theta))=1-F_{X}(\cos(\theta))$

and thus, taking a derivative

$f_{\Theta}(\theta)=f_{X}(\cos(\theta))\sin\theta$

Now define $\Psi_{k}=k\Theta$. We can easily get the density and cumulative
density of this new random variable, as it is just $\Theta$ scaled

$F_{\Psi_{k}}(\psi)=F_{\Theta}(\psi/k)=1-F_{X}(\cos(\theta/k))$

and taking a derivative

$f_{\Psi_{k}}(\psi)=f_{\Theta}(\psi/k)/k=\frac{1}{k}f_{X}(\cos(\psi/k))\sin(\psi/k)$

so we have completed the first step of the process. Now we can compute, for
$T_{k}(X)=\cos(\Psi_{k})$. However, we will have to be more careful with the
transformation. Let $F_{k}$ be the cdf of $T_{k}(X)$, and $f_{k}$ its pdf as
mentioned in the statement. Then

$F_{k}(z)=\Pr(\cos(\Psi_{k})\leq z)$

Let’s look at that inequality in more detail in Fig. 3. For now, assume $k$ is
even:

Figure 3: Cosine inequality visualized. It is satisfied on the regions of the
$x$-axis highlighted in red.

So we can see it is satisfied in the intervals:

$\cos^{-1}(z)\leq\Psi_{k}\leq 2\pi-\cos^{-1}(z)$
$2\pi+\cos^{-1}(z)\leq\Psi_{k}\leq 4\pi-\cos^{-1}(z)$ $\vdots$
$2\pi(j-1)+\cos^{-1}(z)\leq\Psi_{k}\leq 2\pi j-\cos^{-1}(z)$ $\vdots$
$2(k-1)\pi+\cos^{-1}(z)\leq\Psi_{k}\leq k\pi-\cos^{-1}(z)$

Let $m=k/2$. Then, as the intervals are disjoint, we have that

$F_{k}(z)=\Pr(\cos(\Psi_{k})\leq
z)=\sum_{j=1}^{m}\Pr(2\pi(j-1)+\cos^{-1}(z)\leq\Psi_{k}\leq 2\pi
j-\cos^{-1}(z))$

We can express the probability for each summand in terms of the cdf of
$\Psi_{k}$:

(13) $\begin{split}&\Pr(2\pi(j-1)+\cos^{-1}(z)\leq\Psi_{k}\leq 2\pi
j-\cos^{-1}(z))\\\ =&\Pr(\Psi_{k}\leq 2\pi j-\cos^{-1}(z))-\Pr(\Psi_{k}\leq
2\pi(j-1)+\cos^{-1}(z))\\\ =&F_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))-F_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))\end{split}$

so we get

$F_{k}(z)=\sum_{j=1}^{m}F_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))-F_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))$

taking a derivative

(14a) $\displaystyle f_{k}(z)=\sum_{j=1}^{m}f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))\frac{1}{\sqrt{1-z^{2}}}+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))\frac{1}{\sqrt{1-z^{2}}}=$
(14b) $\displaystyle=\frac{1}{\sqrt{1-z^{2}}}\sum_{j=1}^{m}f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))$

Which is what we wanted to show.

Hence we can already see the main part of the pdf we want to reach in the
limit $k\rightarrow\infty$. Therefore, to proof the statement we just need to
show that the sum converges (pointwise) to $1/\pi$. Thus we want to show that
for a fixed $z$,

(15) $\lim_{k\rightarrow\infty}\left\\{\sum_{j=1}^{k/2}f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))\right\\}=\frac{1}{\pi}$

For $k$ odd we just have an extra term in the sum. Before proving the general
case we will look at two particular examples of great interest: $X$ uniformly
distributed and $X\sim\operatorname{Beta}(1/2,1/2)$. For convenience, we
define this sum we are taking the limit as $S_{k}(z)$

$S_{k}(z)=\sum_{j=1}^{k/2}f_{\Psi_{k}}(2\pi
j-\cos^{-1}(z))+f_{\Psi_{k}}(2\pi(j-1)+\cos^{-1}(z))$

## Acknowledgments

We would like to acknowledge the MIT Mathematics Department for their support
during our UROP.

## References

  * [1] J. P. Boyd, Chebyshev and Fourier Spectral Methods Second Revised Edition, Dover Books on Mathematics, Dover Publications, Newburyport, 2nd ed. ed., 2013.
  * [2] S. L. Brunton, M. Budišić, E. Kaiser, and J. N. Kutz, Modern Koopman Theory for Dynamical Systems, Oct. 2021, https://arxiv.org/abs/2102.12086.
  * [3] A. Cadonna, A. Kottas, and R. Prado, Bayesian mixture modeling for spectral density estimation, Statistics & probability letters, 125 (2017), pp. 189–195.
  * [4] L. Fox, Chebyshev polynomials in numerical analysis, Oxford mathematical handbooks, Oxford U.P, 1968.
  * [5] M. J. D. M. J. D. Powell, Approximation theory and methods, Cambridge University Press, Cambridge, 1981.
  * [6] I. Stegun and M. Abramowitz, Handbook of mathematical functions with formulas, graphs, and mathematical tables, Wiley, New York ;, 1964 edition ed., 1972 - 1964.
  * [7] L. N. L. N. Trefethen, Approximation theory and approximation practice, SIAM, Society for Industrial and Applied Mathematics, Philadelphia, extended edition. ed., 2020.


Marek Materzoklogo_ttlM. Antonia Huertas, João Marcos, María Manzano, Sophie
Pinchinat,
François Schwarzentruber54th International Conference on Tools for Teaching
Logic11129TTL2015

# Easyprove: a tool for teaching precise reasoning

Marek Materzok  Institute of Computer Science
University of Wrocław, Poland
<EMAIL_ADDRESS>
###### Abstract.

Teaching precise mathematical reasoning can be very hard. It is very easy for
a student to make a subtle mistake in a proof which invalidates it, but it is
often hard for the teacher to pinpoint and explain the problem in the (often
chaotically written) student’s proof.

We present Easyprove, an interactive proof assistant aimed at first year
computer science students and high school students, intended as a
supplementary tool for teaching logical reasoning. The system is a Web
application with a natural, mouse-oriented user interface.

###### Key words and phrases:

Mathematical logic, Computer science, Proof assistants, Teaching

###### 1991 Mathematics Subject Classification:

F.4.1 Mathematical Logic

##  1\. Introduction

A logic course is an essential part of every computer science curriculum.
Computer science students in University of Wrocław take a mandatory course,
called “Logic for Computer Scientists”, during their first semester. The main
goal of the course is to teach the students the ability to perform precise
mathematical reasoning – which is a very important skill for theoreticians and
practitioners alike. To achieve this goal, the students are given a number of
exercises which involve proving simple theorems, mostly in the domain of set
theory. The students are expected to provide informal proofs in natural
language. The emphasis is placed on logic as a tool for convincing yourself
and others of the validity of mathematical statements, and not on any
particular logical formalism.

The students consider this course to be very hard. During the first few weeks,
they struggle to understand the structure of a mathematical proof. The
teachers do their best to guide them, but the time a teacher can give to an
individual student is necessarily very limited. Therefore there is a strong
need for an educational tool to aid the learning process. Such tool would
serve as a playground, allowing the student to experiment freely with writing
mathematical proofs. It should preferably both constrain the student, so that
only correct proofs are accepted, and suggest him possible ways to continue
the proof if he gets stuck.

There is a class of computer programs called proof assistants, which aid in
formalizing proofs of mathematical theorems; examples include Coq, HOL Light,
Isabelle and Mizar. These tools, while very useful for a specialist, are in
our opinion too complex and quirky to be used for teaching logic to freshmen.
Some have adapted them for use in teaching logic [5, 8, 4, 6]; we believe
these tools are useful only for later stages of student’s education. There
also already exist a number of tools developed specifically as an aid for
teaching logic, such as Jape [2], Yoda [7] and Panda [3], but these tools
focus mostly on teaching logic as a formalism (natural deduction, sequent
calculus, etc.), not as a method of reasoning, as embodied by pen-and-paper
proofs which can be found in mathematical journals.

We developed Easyprove as a supplementary teaching tool to be used in our
logic course for freshmen at the University of Wrocław; we believe it might
also find use in high schools. We briefly summarize our requirements in the
next section.

##  2\. Design goals

In order to be most useful for teaching mathematical reasoning to freshmen,
Easyprove was designed with following goals in mind:

Easy to access.:

A good teaching tool should be easy to access for the student both during
classes and at home. Using contemporary IT technology, the best way to achieve
this is to design the tool as a web application. The Javascript engines of
today’s Web browsers allow to create Web interfaces which are just as usable
as classical “desktop” ones. One can also argue that young people are now very
familiar with Web-like interfaces thanks to the popularity of smartphones and
tablets.

The approach of designing an educational tool as a Web app was successfully
applied by many other projects, including Yoda [7], BoxProvr [4] and ProofWeb
[5].

Natural syntax.:

To use a full-featured proof assistant, the user has to learn a specialized
syntax used for representing terms, proofs and commands for the system. This
can be a big burden for a computer science freshman, who is not yet familiar
with any programming language or other formal syntax.

To remedy this problem, Easyprove presents proofs using a notation close to
natural language, and the terms are displayed using Unicode mathematical
symbols, which are already familiar to the student from mathematics classes.
The symbols can be entered using a graphical keyboard, LaTeX-like shorthands,
or copied-and-pasted from other sources.

Familiar setting.:

Many proof assistants are based on complex formalisms, which can be hard to
understand to freshmen. For example, HOL and Coq use higher-order logics, and
it is typical to encode sets as predicates within the logic. This is often
advantageous for an expert user, but for a beginner it is causing many
unexpected problems: e.g., simple terms like $\\{\\{a\\}\\}\cup\\{a\\}$, which
the student encounters on mathematics classes, give a type error.

In contrast, Easyprove is based on first-order logic and (Zermelo-Fraenkel)
set theory. First-year students should already have some basic familiarity
with them from mathematics classes.

Discoverable user interface.:

Proof assistants have in general a very steep learning curve. Some of them
present a command prompt to the user, who is required to learn a big number of
commands or “tactics” in order to use them (e.g. Coq, HOL Light). Others work
in batch mode – the user has to write a proof script, which is then checked
for correctness by the tool (e.g. Mizar, Isabelle). There are GUI front-ends
available, but these are of little help for learning: they usually list all
possible commands in menus, the commands are not well described, and most of
them are not applicable in a given context.

In contrast, Easyprove presents the user with applicable actions only, and
their effects are completely described. Also, every function of Easyprove is
accessible by the graphical interface, which can be used with only a mouse.

Features for classroom use.:

Easyprove is designed with features important for teachers in mind: creating
task lists, managing student accounts, storing students’ solutions on the
server for review and replay. It also supports internationalization: we have
implemented Polish and English front-end language versions.

In the next section we present how Easyprove meets these design goals by
presenting example interactions with the system.

##  3\. Using Easyprove

To run Easyprove, one enters its URL in any Web browser with standard CSS and
Javascript support. One is then presented with a screen with a list of pre-
entered tasks – theorems to prove. One can also create a new task from
scratch. To create a task, the user has to give it a name, enter the goal
formula, and select the set of assumptions (axioms or lemmas) which will be
available in the task.

###  3.1. Term editor

Figure 1. Term editor

The goal is entered using a graphical term editor (Figure 1). The editor
window has two main parts: on the top is the visual keyboard, which presents
available symbols and variable names present in the current context; the
currently entered term is displayed below it. In the visual keyboard, each
button has a tooltip which displays a short description and presents how a
given symbol can be entered using a keyboard.

The editor has two modes of operation: structural and linear. In the
structural mode, clicking a button on the visual keyboard fills the currently
selected hole in the term, possibly creating new holes for the subterms. When
the user starts typing or clicks on a hole, the editor switches to the linear
mode. The visual keyboard can now be used to insert a symbol in the current
cursor position. Symbols can also be entered by typing a LaTeX-like shorthand,
e.g., typing \forall causes the symbol $\forall$ to appear. Pushing the Enter
button parses the entered term and switches the editor back to visual mode. If
a mistake is made, clicking on a subterm returns it to linear mode for
editing.

###  3.2. Proof editor

Figure 2. Proof editor

The main part of Easyprove is the proof editor. The proof editor screen
(Figure 2) consists of the main block, the sidebar and the toolbar. The main
block presents the proof in a form resembling a pen-and-paper mathematical
proof. The sidebar lists the current goals and the assumptions applicable for
the currently selected goal, which is highlighted. There can be many goals
active, one for each branch of the proof created by case analysis or unproved
lemmas; the user is free to switch between them at any time. The toolbar
contains the undo/redo buttons and a “delete last step in this proof branch”
button.

The formulas occurring in the proof text are of one of two kinds: they can be
either a goal or an assumption. The currently applicable assumptions are
marked with a blue star  ✧; the ones from other proof branches are marked with
a gray star. Unproved goals are marked with a red sad face  ☹; when the goal
is not active, but its proof branch is not yet proved completely, the face
turns yellow  ☹. A proved goal is distinguished by a green happy face  ☺.
Every formula in the proof text is numbered, so that it can be referred to
using this number both in the proof text and in the sidebar.

Initially the proof has only one goal – the theorem one wants to prove – and
no assumptions (the assumptions selected when creating a task are implicit and
are not shown in the proof). To illustrate how one writes a proof in
Easyprove, we use the classical barber paradox as an example. In particular,
we will prove that the existence of a barber which shaves every person that
does not shave himself is paradoxical. This can be stated in first order logic
as:111This sentence can be directly copied from this article’s PDF file and
pasted into the term editor.

$\neg\exists A\forall
B(\textrm{shaves}(A,B)\Leftrightarrow\neg\textrm{shaves}(B,B))$

Interaction with the proof editor is inspired by proof by pointing [1].
Clicking on a subterm of the goal (the subterm currently pointed at is
highlighted) causes a menu window to appear, which lists proof steps
applicable to the selected subterm. In our example, clicking on the whole term
opens the window presented below:

The proof step titled “prove a lemma” is always available, and allows to
introduce lemmas. The next one, “prove by contradiction”, is also always
available, and is the one we want to use here. When the user hovers the mouse
over a proposed proof step, a tooltip appears:

The tooltip briefly summarizes how the proof will be extended if the user
activates the selected proof step. In this case, the negated goal will be
added as an assumption, and the new goal will be $\bot$ – a contradiction.

Clicking on the new assumption will show a proof step named “take this”, which
corresponds to existential quantifier elimination. Selecting this step will
add an assumption about the variable $A$ – which symbolizes the paradoxical
barber:

The new assumption (4) is an universal sentence, so a proof step named
“specialize” is available for it. Choosing it invokes the term editor, which
allows to enter the term used to specialize the universal sentence. Here we
intend to examine the case when the person $B$ is the barber $A$ himself, so
we choose $A$ from the “Variables” tab (the sentence shown next to the button
is the first assumption mentioning this variable):

We get the obviously contradictory sentence
$\textrm{shaves}(A,A)\Leftrightarrow\neg\textrm{shaves}(A,A)$ (the proof state
at this point is shown in Figure 2). Contradiction can be derived from it
either by using a built-in lemma about equivalence, or by case analysis using
the law of excluded middle; we show below the completed proof using the first
possibility:

###  3.3. Proving theorems in set theory

Figure 3. Proof editor – proof in set theory

Easyprove was specifically designed for writing proofs of simple theorems in
set theory. To illustrate its features, we now briefly present a proof that
for every set $A$, the union of all its subsets is equal to $A$; i.e. that
$\bigcup(\mathcal{P}(A))=A$.

Set equality is usually proven using the extensionality principle, or
equivalently by proving two inclusions. Both principles are available as
lemmas in Easyprove, here we choose the second one:

We get a goal which is a conjunction, so we use a proof step named “prove
conjuncts” to prove the conjuncts separately. We can then apply the definition
of set inclusion to both goals (the option to do so is present in the drop-
down menus for the goals):

The proof can easily be completed in this way, by repeatedly applying proof
steps from logic and using set-theoretic definitions and lemmas. A partially
completed proof of the theorem in Easyprove is shown in Figure 3.

##  4\. Implementation

Easyprove is mostly implemented using the programming language Java. The
Google Web Toolkit222http://www.gwtproject.org is used for the user interface,
for communicating with the Easyprove server, and for compiling Java code to
Javascript, which can be executed in a browser. Most of the Easyprove code,
including the proof engine, runs on the client side, which reduces the load
placed on the server and allows easy scaling for large number of users. The
Easyprove server, which manages the task list and user accounts, is
implemented in Scala333http://www.scala-lang.org, and runs on any Java Servlet
container (e.g. Tomcat, Jetty).

The proofs are represented internally as trees, with nodes corresponding to
each proof step used by the user. The nodes may be one of two kinds: they may
represent forward reasoning steps, which add new assumptions, but do not
change the goal; or they can change the current goal or add new goals. Either
way, discarding assumptions (weakening) is prohibited – an introduced
assumption is valid for its entire proof branch. This corresponds to the way
assumptions are usually treated in pen-and-paper proofs. The reasoning rules
implemented in the Easyprove system are sound and complete with respect to the
classical first-order logic.

The new formulas introduced by proof steps (assumptions or goals) are
automatically simplified according to the following rules:

  * •

Expressions with binary logical operators

  * •

Truth $\top$ and falsity $\bot$ symbols are propagated (e.g. $\phi\vee\top$
becomes $\top$) or eliminated ($\phi\wedge\top$ becomes $\phi$) if possible;
$\vee$ and $\wedge$ are reassociated to the left;

  * •

Negations are pushed inwards using the de Morgan’s laws, double negations are
eliminated.

The justification is that a mathematician writing a proof is not concerned
with the particular shape of the formulas he is working with, but with their
meaning.

Assumptions applicable to a clicked subterm on some goal or assumption (see
Section 3.3) are found using pattern matching. For example, the definition of
set inclusion is stored in Easyprove as:

$\forall A\forall B(A\subseteq B\Leftrightarrow\forall x(x\in A\Rightarrow
x\in B))$

The system finds this assumption to be applicable to the goal
$\bigcup(\mathcal{P}(A))\subseteq A$ by matching it to the pattern $A\subseteq
B$, where $A$ and $B$ are considered pattern variables. To make the search for
matching assumptions efficient when the number of them is large, the patterns
are stored in a prefix tree (trie) structure, where the keys are pre-order
representations of the patterns – e.g. $A\subseteq B$ is stored in the prefix
tree as “$\subseteq,A,B$”.

##  5\. Conclusions and future work

We have implemented Easyprove, an easy to use proof assistant, as an aid for
teaching logical reasoning. It is targeted for first year computer science
students and high school students. The system is currently in prototype stage
and requires further work in order to be fully usable. The goals for future
development are:

Other axiom systems.:

Easyprove can be in principle extended to handle axiomatic systems other than
set theory – for example, Hilbert’s axioms for Euclidean geometry. Such an
extension would enhance the educational utility of the tool.

Better proof editor.:

The proof editor does not currently allow easy modification of the proof: the
only way to restructure an already entered part of the proof is to undo the
most recent proof step in a proof branch. A user interface for restructuring a
proof would aid active experimentation, and therefore improve the learning
experience.

More use of natural language.:

Easyprove currently presents formulas in symbolic form. Adding an option to
present them in natural language instead (e.g. instead of $\forall x\
\textrm{shaves}(x,y)$ write “for all $x$, $x$ shaves $y$”) would help the
student make the connection between what he sees on screen and actual pen-and-
paper mathematical proofs.

Proof automation.:

The main priority in Easyprove’s design was handling short proofs of simple
theorems well, because these are most instructive for teaching logical
reasoning. Because of this decision, writing longer proofs in Easyprove is
tedious. It remains to be explored how one can include automation in Easyprove
without hurting its didactic character.

Mobile interface.:

Easyprove was designed with a traditional keyboard and mouse in mind. Given
the recent popularity of touch screen devices, a redesign of the user
interface to accommodate them would certainly allow Easyprove to reach a wider
audience.

Nevertheless, the system has proven to be usable in its current state. It was
not used in the classroom yet, but it was presented to selected students and
their response was positive.

The readers are invited to try out Easyprove. The current stable version of
the system is available online at http://easyprove.ii.uni.wroc.pl/.

## References

  * [1] Yves Bertot, Gilles Kahn, and Laurent Théry.  Proof by pointing.  In Masami Hagiya and John C. Mitchell, editors, Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS’94), volume 789 of Lecture Notes in Computer Science, pages 141–160. Springer, 1994.
  * [2] Richard Bornat and Bernard Sufrin.  Jape: A calculator for animating proof-on-paper.  In William McCune, editor, Automated Deduction—CADE-14, volume 1249 of Lecture Notes in Computer Science, pages 412–415. Springer Berlin Heidelberg, 1997.
  * [3] Olivier Gasquet, François Schwarzentruber, and Martin Strecker.  A Proof Assistant in Natural Deduction for All. A Gentzen style proof assistant for undergraduate students.  In P. Blackburn, H. van Ditmarsch, M. Manzano, and F. Soler-Toscano, editors, Proceedings of the Third International Congress on Tools for Teaching Logic (TICTTL’11), volume 6680 of Lecture Notes in Computer Science, Salamanca, Spain, June 2011.
  * [4] Jonas Halvorsen.  Web based GUI for natural deduction proofs in Isabelle.  Master’s thesis, University of Edinburgh, 2007.
  * [5] Maxim Hendriks, Cezary Kaliszyk, Femke van Raamsdonk, and Freek Wiedijk.  Teaching logic using a state-of-the-art proof assistant.  Acta Didactica Napocensia, 3(2):35–48, June 2010.
  * [6] H. James Hoover and Piotr Rudnicki.  Teaching freshman logic with Mizar-MSE.  In Workshop on Teaching Logic and Reasoning in an Illogical World, Piscataway, New Jersey, July 1996.
  * [7] Benjamín Machín and Luis Sierra.  Yoda: a simple tool for natural deduction.  In P. Blackburn, H. van Ditmarsch, M. Manzano, and F. Soler-Toscano, editors, Proceedings of the Third International Congress on Tools for Teaching Logic (TICTTL’11), volume 6680 of Lecture Notes in Computer Science, Salamanca, Spain, June 2011.
  * [8] Jakub Sakowicz and Jacek Chrząszcz.  Papuq: a Coq assistant.  In H. Geuvers and P. Courtieu, editors, Proceedings of PATE’07 International Workshop on Proof Assistants and Types in Education (PATE’07), pages 79–96, Paris, France, June 2007.