In principle, yes.

I am not a lean expert, but I imagine that python primitives like dicts, ints, functions, etc., have been defined in lean. So if you add a way to annotate python code with a proof, you should as well be able to automatically translate it to Lean completely.

it's a matter of how much of a modeling gap do you choose to accept.

for full, honest to god, end to end verification this would be insufficient. but you don't need that in order to reap benefits.

just gotta make sure you actually bound the triage process with some sort of automated verification process. like comparative test cases or similar. otherwise it's just a particularly expensive way of agentic hallucination.