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---
Xeraser :RepubblicaSocialeItaliana: :israelflagburn: @Xeraser@detroitriotcity.com (2026-10-10 08:29:43)
@icedquinn @sun
you should throw glm in the trash because it's literally "we have claude opus at home"
deepseek is the chink model you should bet on
Reply
---Replies---
Q.U.I.N.N.@icedquinn@blob.cat (2026-10-10 08:35:59)
@Xeraser @sun i think i tried deepseek-r1 when it came out. it was too heavily censored to be much fun.