Home | Notifications | New Note | Local | Federated | Search | Logout
Note Detail
Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-10-10 07:18:57)
@sun i haven't seen it, no. i've been adjacent to the proof space recently though. Maude is used for defense verification. (though i'm trying to use maude for codegen, which ran in to some stupid errors.)
there is a controversy right now, though, because openai is flooding math papers with bad proofs.
---Reply---
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
---Replies---
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
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