Comment by kurtis_reed

Yes however, whether a natural language proof and a formal proof "correspond" is subjective.