Not yet, but it's definitely something worth experimenting. FWIW, there are precedents to this, e.g. Coq developers typically write the types and (when they're

Not yet, but it's definitely something worth experimenting. FWIW, there are precedents to this, e.g. Coq developers typically write the types and (when they're lucky) have "strategies" that write the bodies of functions. This was before LLMs, but now, some people are experimenting with using LLMs for this: https://arxiv.org/abs/2410.19605 https://arxiv.org/abs/2410.19605