>fwiw I have a bunch of LLMs writing first Lean code

How do you bridge the mental gap?

The gap between me writing high quality rust do this steps and something being logically sound seems enormous to me

Maybe I'm misunderstanding things but I just can't articulate my ideas in casual lean4. But i can do casual rust spec

As someone experimenting with this, it's definitely very difficult to articulate your ideas using advanced type systems. At the same time, the process of doing it often forces me to seriously think through what I want the code to do, which I've noticed qualitatively improves the end result and my understanding of it.

My advice is to be okay with starting small: don't go for full end-to-end correctness or anything like it. Just think of simple properties you want like 'the list returned by this endpoint should always be sorted in ascending order' or 'this operation should be idempotent' and go from there. Use your favorite LLM to help come up with example specifications from natural language, as a starting point, and try hard to fully understand those.

This kind of work does operate at the frontier of what LLMs can do, so expect to run into roadblocks (wasting tokens proving accidentally hard properties, etc).