|
|
|
|
|
|
by forward-slashed
972 days ago
|
|
|
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. https://x.com/morph_labs |
|
|