Hi,
I have been thinking
to this issue for years (decades?). In France we have this research
agency INRIA which has been supporting the Coq project for decades,
leading to a fairly "good quality software" (in my opinion). Say twenty
years ago, the Coq project was targetting the computer science community
and was not ready to "attack" the mathematical community. From this side,
the picture seems much better nowadays.
A possible strategy toward the investment of the mathematical community is as follows:
------------------------
1-
create a body tying (part of) this community with for instance (part
of) the Coq project (and/or the Agda project, about which I know
little).
2- obtain specific funding from a Research Agency
(NSF, CNRS?) for partly formalized PhD fellowships, together with companion funding for the
technical support (eg from the Coq team) to the (partial) formalization.
3- obtain good applications, coming from ouside this community.
4-
select the winning applications regarding both the interest of the
naked thesis, and the feasability of the (partial) formalization.
5- help collectively the success of each selected project.
6- Write assessments in particular for the formalization efforts of these newage doctors, so that they win positions whenever they deserve.
---------------------------
I leave it here.