Some time ago I started designing a system that would convert between automated checkers syntax and some simplified human-readable English. But failed, once realized the problem is bigger than me.

Here I just want to encourage anyone who thinks he's a good programmer to develop such a system. It would be extremely useful for education as well: students would get a tool that explains complex proofs, and professors would give assignments to put a theorem into the system (if student is able to enter the theorem into the system, then he/she definitely understands it up to the very foundations). The main problem to solve is good UX, not the math.

They who manage to make the system, the new verified Wikipedia for Math, would have their names inscribed for eternity, because Math is eternal.

yes, that's why I think something different than Automated proof checking for solving advanced theorems, you need to have an AI that can take "creative leaps" and break down proofs down to something humans can understand, and not just verify existing rules