Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-10-10 07:21:30)
@sun i think i've poke claude (but not GLM as much) about it. Lean upstream uses LLMs for proofs, but its safe to do this. they write the term to be proven by hand and let the LLM close it. so the LLM never controls the end goal and the kernel validates intermediate steps are valid.

it is less safe if the LLM is writing the goal because you can--even with dependent types--make a spec that is ass trash and worthless.
---Reply---
Blurry Moon@sun@shitposter.world (2026-10-10 07:22:18)
@icedquinn oh yes I am aware, I try to spot-check just the regular tests that I have the AI generate for me and I always find ones that are bullshit