Comment by famouswaffles

No it's already explicitly stated that translation to lean is a second step that happens after NL proof is done. That's why some of 400 paper dump is without lean proofs.