Lean 4 seems to be pretty AI-usable, and you get insane guarantees (but LLM do seem to make very heavy use of "sorry")