[ykonstant]

This workflow is an explicit goal of the Lean 4 devs. The official Zulip chat has a channel dedicated to the interface between the two:

https://leanprover.zulipchat.com/#streams/219941/Machine%20L...

[cubefox]

That would be interesting, though this link requires an account.