Lean 4 seems to be pretty AI-usable, and you get insane guarantees (but LLM do s...

		tatjam 8 days ago \| parent \| context \| favorite \| on: If you're going to vibe code, why not do it in C? Lean 4 seems to be pretty AI-usable, and you get insane guarantees (but LLM do seem to make very heavy use of "sorry")