去开一个类似GitHub的网站，姑且叫他MathHub.
网站分成两部分：一部分是形式证明，提供写形式证明的教学以及类似于GitHub的形式证明内容托管服务；另一部分用来发表论文。前期的投入不小，因为要募集一些程序员开发并维护一个好用的Coq的前端（现在的Coq对非理论cs领域的数学家过于不友好），启动一个将现有的大部分数学成果形式化的项目，当然还得做很多宣发。网站的两部分后期要融合起来，理想状况是每一篇发表的论文附带一个形式证明的repo，里面是所有证明步骤；形式证明在发表时由机器检查。
一亿人民币节省一点用维持几年应该还是有的，这段时间里争取做完前期任务并在数学界获得声望。因为MathHub上面的论文的正确性由机器验证保证，审稿又快，还对所有人免费开放，相比于传统的学术期刊优势很明显。有了足够的声望之后就可以过渡到以国家提供的科研经费运行。
如果一切顺利，十年以后大部分的数学成果都以形式证明发表在MathHub上。天下苦学术出版商久矣，MathHub能为各高校和研究院节省下的购买期刊数据库的钱（最终也是来自于国家给的经费）用来维持MathHub的运行，相比学术期刊的方式效率能提升很多。而且MathHub上的证明是机器可读的形式，可以用推荐算法来给学者推送感兴趣的领域的最新成果；甚至这些证明可以用作研发自动证明系统的训练数据。
人类的认知和阅读能力都是有极限的，未来的数学研究必然是人和计算机深度合作的工作。自动证明系统超越人类在可预见的未来也是必然会发生的事情。开MathHub的这一亿元人民币将会是人类历史上最伟大的一笔投资，心动不如行动吧！（逃
