One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans.
Generally, most computer scientists using proof automation don't care about the proof itself -- they care that one exists. It can contain as many lemmas and steps as needed. They're unlikely to ever read it.
It seems to me that LLMs would be decent at generating proofs this way: so long as they submit their tactics to the proof checker and the proof is found they can generate whatever is needed.
However for mathematicians, of which I am not a member of that distinguished group, seem to appreciate qualities in proofs such as elegance and simplicity. Many mathematicians that I've heard respond to the initial question believe that a proof generated by some future AI system will not be useful to humans if they cannot understand and appreciate it. The existence of a proof is not enough.
Now that we're getting close to having algorithms that can generate proofs it makes the question a bit more urgent, I think. What use is a proof that isn't elegant? Are proofs written for a particular audience or are they written for the result?
I wonder if he’s familiar with Peirce’s alpha existential graphs. They are a complete propositional logic with a single axiom and, depending how you count them, 3-6 inference rules. They use only negation and conjunction.
They also permit shockingly short proofs compared to the customary notation. Which, incidentally was also devised by Peirce. Peano freely acknowledges all he did is change some of the symbols to avoid confusion (Peirce used capital sigma and pi for existential and universal quantification).
Perhaps using Grobner basis for formal proofs [1],[2] could be similar to what appears here, that is during the proof the length of the terms (or polynomials) can grow and then at the end there is a simplification and you obtain a short grobner basis (short axioms).
A simple question, since • is nand, the theorem ((a•b)•c)•(a•((a•c)•a))=c, can be proved trivially computing the value of both sides for the 8 values of a,b,c. Also there are 2^(2^2)=16 logic functions with two variables so is trivial to verify that the theorem is valid iff • is nand.
Perhaps the difficulty is proving the theorem using rules?, there must be something that I don't see (I just took a glimpse in a few seconds).
It's interesting how sometimes it feels like a topic starts showing up super often all of the sudden. It probably isn't a coincidence, since my interest and probably this post's interest is due to Tao's recent equation challenge https://teorth.github.io/equational_theories/ .
I was surprised and intrigued to find Wolfram's name when I was reading background literature doing this blog post https://www.philipzucker.com/cody_sheffer/ where I translated my friend's Lean proof of the correspondence of Sheffer stroke to Boolean algebra in my python proof assistant knuckledragger https://github.com/philzook58/knuckledragger (an easier result than Wolfram's single axiom one).
I was also intrigued reading about the equational theorem prover Waldmeister https://www.mpi-inf.mpg.de/departments/automation-of-logic/s... that it may have been acquired by Mathematica? It's hard to know how Mathematica's equational reasoning system is powered behind the scenes.
Mathematica can really make for some stunning visuals. Quite impressive.
agentultra ·6 days ago
Generally, most computer scientists using proof automation don't care about the proof itself -- they care that one exists. It can contain as many lemmas and steps as needed. They're unlikely to ever read it.
It seems to me that LLMs would be decent at generating proofs this way: so long as they submit their tactics to the proof checker and the proof is found they can generate whatever is needed.
However for mathematicians, of which I am not a member of that distinguished group, seem to appreciate qualities in proofs such as elegance and simplicity. Many mathematicians that I've heard respond to the initial question believe that a proof generated by some future AI system will not be useful to humans if they cannot understand and appreciate it. The existence of a proof is not enough.
Now that we're getting close to having algorithms that can generate proofs it makes the question a bit more urgent, I think. What use is a proof that isn't elegant? Are proofs written for a particular audience or are they written for the result?
Show replies
User23 ·6 days ago
They also permit shockingly short proofs compared to the customary notation. Which, incidentally was also devised by Peirce. Peano freely acknowledges all he did is change some of the symbols to avoid confusion (Peirce used capital sigma and pi for existential and universal quantification).
Show replies
coonjecture ·6 days ago
A simple question, since • is nand, the theorem ((a•b)•c)•(a•((a•c)•a))=c, can be proved trivially computing the value of both sides for the 8 values of a,b,c. Also there are 2^(2^2)=16 logic functions with two variables so is trivial to verify that the theorem is valid iff • is nand. Perhaps the difficulty is proving the theorem using rules?, there must be something that I don't see (I just took a glimpse in a few seconds).
Automatic formal proofs can be useful when you are able to test [1] https://doi.org/10.1016/j.jpaa.2008.11.043 [2] https://ceur-ws.org/Vol-3455/short4.pdf
Show replies
bmc7505 ·6 days ago
Show replies
philzook ·6 days ago
I was surprised and intrigued to find Wolfram's name when I was reading background literature doing this blog post https://www.philipzucker.com/cody_sheffer/ where I translated my friend's Lean proof of the correspondence of Sheffer stroke to Boolean algebra in my python proof assistant knuckledragger https://github.com/philzook58/knuckledragger (an easier result than Wolfram's single axiom one).
I was also intrigued reading about the equational theorem prover Waldmeister https://www.mpi-inf.mpg.de/departments/automation-of-logic/s... that it may have been acquired by Mathematica? It's hard to know how Mathematica's equational reasoning system is powered behind the scenes.
Mathematica can really make for some stunning visuals. Quite impressive.