Also check out Morph Labs, which is working with Lean to create an AI proof assistant. Cool startup by ex-OpenAI folks.
Essentially a strong type system of Lean can help with constrained generation. Thus every token would always lead to some valid (if not correct) proof in Lean, iiuc. Maybe people @ Morph can comment.