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.
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.
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".
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.
Exactly. If humans were good at writing proofs, they'd just write the code.