Why is there not a system for computer checking mathematical proofs yet (2018)? [closed]

Solution 1:

Have a look into the Flyspeck Project in which the proof of Kepler's sphere-packing conjecture was checked by computer precisely to avoid the problems that Martin Argerami denies in the human review process, but are significant in problems whose solution necessarily involves computation.

Solution 2:

They haven't been forgotten - These systems are still being actively researched and developed. I personally know someone who is working on the Lean theorem prover. In addition you can see Coq is being actively developed.

Solution 3:

I would suggest having a look at Freek Wiedijk's list tracking which of the "top 100 mathematical theorems" have so far been formalized in various theorem prover/theorem checker systems such as HOL, Isabelle, COQ, Mizar, Metamath, ProofPower, nqthm/ACL2, PVS, and NuPRL/MetaPRL.

http://www.cs.ru.nl/~freek/100/

And also "what might be the smallest proof checker" (500 lines of python):

https://en.wikipedia.org/wiki/Metamath#Proof_checkers

Those should give you hours (if not days) of reading material :-)