  The 9th International Workshop on Theorem-Proving Components for Educational
Software (ThEdu'20) was scheduled to happen on June 29 as a satellite of the
IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by
surprise, though, and the main conference was virtualised. Fearing that an
online meeting would not allow our community to fully reproduce the usual
face-to-face networking opportunities of the ThEdu initiative, the Steering
Committee of ThEdu decided to cancel our workshop. Given that many of us had
already planned and worked for that moment, we decided that ThEdu'20 could
still live in the form of an EPTCS volume. The EPTCS concurred with us,
recognising this very singular situation, and accepted our proposal of
organising a special issue with papers submitted to ThEdu'20. An open call for
papers was then issued, and attracted five submissions, all of which have been
accepted by our reviewers, who produced three careful reports on each of the
contributions. The resulting revised papers are collected in the present
volume. We, the volume editors, hope that this collection of papers will help
further promoting the development of theorem-proving-based software, and that
it will collaborate to improve the mutual understanding between computer
mathematicians and stakeholders in education. With some luck, we would actually
expect that the very special circumstances set up by the worst sanitary crisis
in a century will happen to reinforce the need for the application of certified
components and of verification methods for the production of educational
software that would be available even when the traditional on-site learning
experiences turn out not to be recommendable.
