Unless the proofs themselves are defined with natural language, I don't see them being adopted by humans. It takes a high cognitive load to read let alone write a proof.

▲

chinabot 3 hours ago | parent [-]

Agree, but natural languages have ambiguity, the AI output should really include the assumptions and we seriously need to replace the word "prompt" with "conversation".

	▲	tonic_note 2 hours ago \| parent \| next [-]
		I think a big issue we keep running into is this idea that language is ambiguous but code is somehow not. Code is merely an extension of language, a DSL if you will. Implicit assumptions become baked into the logic of the code and those assumptions can be wrong. Look at the guy whose AI changed the entire rules of the game to avoid breaking the law. Was that really the desired outcome? And the more you try to lock it down the more language you add and therefore more ambiguity and assumptions. You cannot solve the problems of language with more language.
	▲	docheinestages 3 hours ago \| parent \| prev [-]
		Exactly. If humans were good at writing proofs, they'd just write the code.