Convincing mathematicians about it is a really old problem. Here's the first paper I saw really describing how mathematics has been done as a social process foc

Convincing mathematicians about it is a really old problem. Here's the first paper I saw really describing how mathematics has been done as a social process focused on people's understanding: https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf A 2009 rebuttal to be fair to my side of the debate: https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=400A0F7C050239C990098177E0C7FBA8?doi=10.1.1.150.4680&rep=rep1&type=pdf https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=40... Here's a recent article about the situation from yet another segment of people trying to bring in automation: https://www.quantamagazine.org/in-computers-we-trust-20130222/ https://www.quantamagazine.org/in-computers-we-trust-2013022... Unlike article's impression, a lot of how to build trustworthy provers has already been solved. The state-of-the-art is probably Milawa: a prover for ACL2-like logic running on a Lisp verified down to the machine code. It has summaries of various approaches of making computational math/logic trustworthy: https://www.kookamara.com/jared/2015-jar-milawa.pdf https://www.kookamara.com/jared/2015-jar-milawa.pdf Note: Like in Common Criteria EAL7 or DO-178C, I'd use a mix of techniques for verification instead of blindly trusting the math. Lots of human review, static analysis, testing, etc. Far as projects implementing math's foundations, you should especially check out Mizar (most complete) and Metamath (open source): https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Metamath https://en.wikipedia.org/wiki/Metamath If authors give permission, it might be worthwhile to attempt to create re-writing tools that convert those tools languages into platforms in use by programmers. That's mainly Coq, the HOL's, Why3, and (hardware) ACL2. I don't know how feasible that is. I just think it could be valuable.