It's almost always easier to understand theorems than proofs. People could be writing down properties of their programs and the AI could generate a proof or produce a counterexample. It is not necessary to understand the proof in order to know that it is correct.
At least in principle. Practically, any system as least as powerful as first-order logic is undecidable, so there can never be any computer program that would be able to do this perfectly. It might be that some day, an AI could be just as good as a trained mathematician, but so far, it doesn't look like it.
> It might be that some day, an AI could be just as good as a trained mathematician, but so far, it doesn't look like it.
One of the on-going arguments in automated theorem proving has been this central question: would anyone understand or want to read a proof written by a machine?
A big part of why we write them and enjoy them is elegance, a rather subjective quality appreciated by people.
In computer science we don't tend to care so much for this quality; if the checker says the proof is good that's generally about as far as we take it.
But endearing proofs that last? That people want to read? That's much harder to do.
I had mentioned that. This is true today when software developers are writing proofs and why automation is useful.
You would still need to be able to read the proof that a computer generated and understand what it contains in order to judge whether it is correct with respect to your specifications. So in some sense elegance would be useful since the proof isn’t written by a human but has to be understood by one.
If the input here is still plain language prompts… then we’ll have to assume that we eventually develop artificial cognition. As far as I know, there isn’t a serious academic attempting this, only VC’s with shovels to sell.
I might also add that, “they,” on the first line are software developers. Most are not trained to read proofs. Few enough can write a good test let alone understand when a test is insufficient evidence of correctness.
I had to learn on my own.
Even if LLMs could start dropping proofs with their PRs would they be useful to people if they couldn’t understand them or what they mean?
Yeah, people fixated on the meaning of "makes no sense" to evade accepting that the proofs LLMs output are not useful at all.
On a similar fashion, almost all LLM created tests have negative value. They are just easier to verify than proofs, but even the bias into creating more tests (taken from the LLM fire hose) is already harmful.
I am almost confident enough to make a similarly wide claim about code. But I'm still collecting more data.
Whether it's something you care about, or even something that should be true at all is out of scope.