Finally, Lucas implicitly assumes that if the mind is a formal systems, then our “seeing” a statement to be true involves the statement being proved in that formal system.

To me this seems like the crux of the issue (in fact, I perceive it to be the crux of the issue, so QED). Of course there are LW posts like Your Intuitions are not Magic, but surely a computer could output something like "arithmetic is probably consistent for the following reasons..." instead of a formal proof attempt if asked the right question.