[Axiom-developer] The QED Manifesto

[Tim Daly]

This was mentioned in the video.
https://www.cs.ru.nl/~freek/qed/qed.html

One of Axiom primary goals seems to fit the QED third goal:

The third motivation for the QED project is education. Nothing is more
important than mathematics education to the creation of infrastructure
for technology-based economic growth. The development of mathematical
ability is notoriously dependent upon "doing" rather than upon "being
told" or "remembering". The QED system will provide, via such
techniques as interactive proof checking algorithms and an endless
variety of mathematical results at all levels, an opportunity for the
one-on-one presenting, checking, and debugging of mathematical
technique, which it is so expensive to provide by the method of one
trained mathematician in dialogue with one student.

Also, the development of Axiom as free and open source addresses this objection:

Objection 2. Intellectual property problems. Such an enterprise as QED
is doomed because as soon as it is even slightly successful, it will
be so swamped by lawyers with issues of ownership, copyright, trade
secrecy, and patent law that the necessary wide cooperation of
hundreds of mathematicians, computer scientists, research agencies,
and institutions will become impossible.

Reply to Objection 2. In full cognizance of the dangers of this
objection, we put forward as a fundamental and initial principle that
the entirety of the QED system is to be in the international public
domain, so that all can freely benefit from it, and thus be inspired
to contribute to its further development.

Axiom certainly does not address the whole of QED. At most Axiom will likely be
viewed as an primitive first step on a long path.