6 ms·
Lean 4 seems to be pretty AI-usable, and you get insane guarantees (but LLM do seem to make very heavy use of "sorry")
by tatjam 10mo ago
Lean 4 seems to be pretty AI-usable, and you get insane guarantees (but LLM do seem to make very heavy use of "sorry")