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