The process should now be: write your specs in lean, LLMs fill the gaps, then you translate the proof into your end product software. Otherwise LLMs will simply keep finding bugs, both in old and new code.
You assume lean can express more than it can.
Feel like “translating the proof into your end product” is a bit of a “draw the rest of the owl”