What's so hard about creating a piece of software with as minimal as possible mathematical axioms, defining a formal language in which one can create new constructs based on the existing ones, and then all research papers could be written in that language and its correctness verified by a computer?
Computer-Assisted Proof is a rather old field of research, and programs of that kind have already been made. Most of them relied on brute-force approaches, or graph search algorithms (BFS, DFS).
The thing is, first of all, it would not be trivial to define a language that can describe every possible problem (see: incompleteness theorems), and also, assuming you defined that language and found an optimal way to catch up with the current state of research, what would happen if you fed your magic algorithm a paper describing the correctness of the magic algorithm itself?
Edit: As mentioned by Steven, the obvious problem with this is that one would have to insert each and every proof by hand, so I assumed OP wanted to generate those proofs in a less "manual" way. Either way, the problem of defining such a language would still be a thing (an example of a failed attempt at that might be Russell's Principia).