The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 p

The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.