This happens all the time with human researchers.

e.g. one of the lemmas in the NL description is false, but a weaker version of the lemma (that does hold) is sufficient for the proof, so the (incorrect) lemma is never formalized.