How would that be different from something like ChatGPT executing Lean? That's exactly what humans do, we have messy reasoning that we then write down in formal logic and compile to see if it holds.