I think he accounts for that in the answer, "in a way that would be faster than if one or both proofs were informal" (which assumes "one formal and one informal" is also a case he's talking about). The way I understand his point is that in either case you would have to go through the two mathematical structures with the same amount of rigour and attention until you find the divergence, and that's easier to do when at least one side is formal (but can be done in either case).

In other words, informal math doesn't make this problem easier because you can still make and miss mistakes in encoding intent into the structure. But at least with formal math, there's whole classes of mistakes that you can't make.