8 ms·

Who Can Understand the Proof? A Window on Formalized Mathematics

190 points by ColinWright 2y ago

cbm-vic-20 2y ago
[flagged]
- deleted 2y ago
  [deleted]
francasso 2y ago
Is there a relation between the "single axiom for boolean algebra" that Wolfram claims to have discovered and the fact that you can express all boolean operations with just NAND?
- ur-whale 2y ago
  > Is there a relation between the "single axiom for boolean algebra" that Wolfram claims to have discovered and the fact that you can express all boolean operations with just NAND? Seems to be partially answered in the article. Search for "Is There a Better Notation?"
- markisus 2y ago
  I was sort of puzzled by the meaning of "axiom for boolean algebra" as well, and I looked into this more. The way I learned boolean algebra was by associating certain operations (AND, NOT, OR, etc) to truth tables. In this framework, proving a theorem of boolean algebra would just involve enumerating all possible truth assignments to each variable and computing that the equation holds. There is another framework for boolean algebra that does not involve truth tables. This is the axiomatic approach [1]. It puts forth a set of axioms (eg "a OR b = b OR a"). The symbol "OR" is not imbued with any special meaning except that it satisfies the specified axioms. These axioms, taken as a whole, implicitly define each operator. It then becomes possible to prove what the truth tables of each operator must be. One can ask how many axioms are needed to pin down the truth table for NAND. As you know, this is enough to characterize boolean algebra, since we can define all other operators in terms of NAND. It turns out only one axiom is needed. It is unclear to me whether this was first discovered by Wolfram, or the team of William McCune, Branden Fitelson, and Larry Wos. [2] [1] https://en.wikipedia.org/wiki/Boolean_algebra_(structure) https://en.wikipedia.org/wiki/Boolean_algebra_(structure) [2] https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_algebra#:~:text=In%20mathematical%20logic%2C%20minimal%20axioms https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_alg...,.
  - jarpschope 2y ago
    Thanks for the wonderful explanation brother!
  - rramadass 2y ago
    Nice comment explaining the difference between two viewpoints. The former one is set theoretic i.e. set of objects (eg. terms) and operations (eg. and/or/not) defined on those objects. The latter is an algebraic specification where a number of properties (expressed by logical formulas which can be axioms or theorems) are expected to be satisfied by the operations. Also see https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_algebra https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_alg... PS: I would take any claim by Stephen Wolfram as having been "the first" to discover anything with a boatload of salt.
- Tainnor 2y ago
  The latter is a necessary, but not sufficient condition for the former.
ur-whale 2y ago
Here's a meta question about this article: let's try to estimate how many people on earth, say within the next 5 years will ever read the entire article in all of its gory details? These days, an LLM will, perhaps. An make it palatable to puny humans.
- deleted 2y ago
  [deleted]
- philipwhiuk 2y ago
  Or maybe it will fail to recall all of it and make something up. Because it has 300B parameters not infinitely many. We currently pull out our phones at the pub/table to check something someone makes up to see if it's legitimate. Now we've invented the technology to have something be that thing that creates a half-truth from what it has absorbed.
- astrange 2y ago
  Just train the LLM search engine to tell people it contains the answers to all their questions.
- queuebert 2y ago
  I probably could, but I'm 99% sure it's a thinly veiled self promotion, as is usual from him.
cjfd 2y ago
What is this central dot? I thought a central dot in boolean logic means logical and but then the axiom is clearly false..... I don't get what this is about.
- ur-whale 2y ago
  > What is this central dot? Yeah, I wish he had started by defining that. The is hard to understand without it. Search for "Is There a Better Notation?" in the article, it seems "." is NAND
  - hulium 2y ago
    Technically, his axiom is the definition for what the operator is. Any set together with an operator "•" that satisfies this law is a boolean algebra. Binary logic where •=NAND is one such example because it satisfies the axiom.
  - NooneAtAll3 2y ago
    it's simply "Generic Operator". The only requirements is to follow axioms for all its input values. NAND isn't THE operator, it is AN operator that can be in that place. If there's only 1 value that variables can be - "I", then "I \dot I = I" would be a valid operator that follows given axioms
- larschdk 2y ago
  The source uses ○, not •, for the NAND operation.
- BetterWhisper 2y ago
  In "The proof as we know" section he states that the dot is a NAND operation Quote: "the · dot here can be thought of as representing the Nand operation"
- Tainnor 2y ago
  As others have already said, think of it as NAND, although in traditional logic this is typically called the "Sheffer stroke".
robertkoss 2y ago
As someone who is completely unrelated to the academic world, is Stephen Wolfram actually working on meaningful things? I remember reading an article where he was announcing his Physics Project which got a lot of backlash from the scientific community (at least I think that was the case). Nonetheless, every time I browse through Wolfram Alpha I am thoroughly impressed of what it can do with only Natural Language as an input.
- meltyness 2y ago
  They've got a YouTube with pretty robust updates. Iirc, during the lock downs, he'd do live coding and stuff.
- deleted 2y ago
  [deleted]
- pvg 2y ago
  https://hn.algolia.com/?dateRange=all&page=0&prefix=false&query=by%3Adang%20wolfram%20derangement&sort=byDate&type=comment https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
  - Tainnor 2y ago
    That's weird, why does Stephen Wolfram gets some sort of special treatment here that nobody else seems to get - including people that are subject to much more common and intense criticism (just the other day there were people bitching about Trudeau, for example - or let's take Elon Musk who is an asshat (IMHO, YMMV), is discussing that off-topic when it comes to how he manages Twitter?). The question "is Stephen Wolfram being taken seriously by the mathematics community?" seems relevant as a question to gauge whether one should spend time reading a very long article. edit: an even more relevant analogy - is Mochizuki's big ego irrelevant in a discussion about whether his proof of the abc conjecture, that nobody understands and which he refuses to explain properly, is correct?
    - pvg 2y ago
      Because it's highly repetitive and uninteresting, especially in the context of an article that is not about Wolfram. The mod exhortations are a consequence of the repetitiveness rather than some special carveout. Other things that get that repetitive get similar appeals.
bmc7505 2y ago
Although Wolfram doesn't mention it by name, this is closely related to what he is trying to do: https://en.wikipedia.org/wiki/Reverse_mathematics https://en.wikipedia.org/wiki/Reverse_mathematics
- deleted 2y ago
  [deleted]
- vasco 2y ago
  Wanted to thank you for the share, added "Reverse Mathematics: Proofs from the Inside Out" to my reading list which was referenced in the article you posted: https://www.goodreads.com/book/show/34928283-reverse-mathematics https://www.goodreads.com/book/show/34928283-reverse-mathema...
  - bmc7505 2y ago
    Depending on how comfortable you are with model theory you might also enjoy Dzhafarov and Mummert’s textbook, which first brought the subject to my attention.
sylware 2y ago
Formal proof is so much important, since currently maths is built on set theory, I wonder how the set theory axioms are written in some of the formal solvers.
- robinzfc 2y ago
  No need to wonder for long, just have a look. Metamath: https://us.metamath.org/mpeuni/mmset.html#axioms https://us.metamath.org/mpeuni/mmset.html#axioms Isabelle/ZF: https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html
- gaogao 2y ago
  You can model types as a set and sets as types in many ways, so a number of the basic set theory axioms are pretty simple to express as lemmas from type axioms. IIRC you get constructive set theory easy, but do have to define additional axioms typically for ZFC.
  - JonChesterfield 2y ago
    The C part of ZFC is a challenge for constructive theories
    - sylware 2y ago
      I recall that you really need the "C" from ZFC or you'll end-up with a much less comfy realm of mathematics. So the "C" from ZFC is "challenging" for type theory? Because, and I think I am not that much overshooting, fundamental axioms are really, really simple, even the "C" from ZFC, and if is "challenging" to express it using some fundamental theory, well, not good omens for that theory, or they can rebuild the realm of classic maths with their own "C"??
      - JonChesterfield 2y ago
        The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world of ZFC. I expect there's an equivalent addition to constructive type theory that yields non-constructive type theory. Adding more axioms isn't necessarily making systems better though.
deleted 2y ago
[deleted]
agentultra 2y ago
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?
- Davidbrcz 2y ago
  It depends. A proven conjecture is IMO better than an unproven one. But usually, a new proof would shed new lights or build bridges between concepts that were before unrelated. And in that sense, a proof not understandable by humans is disappointing, because it doesn't really fullfil the need to understand the reason behind why it's true.
- crabbone 2y ago
  This isn't a new conundrum. This was a very contentious question in the end of the 19th century, where French mathematicians clashed with the German mathematicians. Poincare is known for describing proofs as texts intended to convince other mathematicians that something is the case, whereas Hilbert believed that automation is the way to go (i.e. have a "proof machine", plug in the question, get the answer and be done with it). Temporarily, Germans won. Personally, I don't think that proofs that cannot be understood have no value. We rely on such proofs all the time in our day-to-day interpretation of the world around us, our ability to navigate it and anticipate it. I.e. there's some sort of an automated proof tool in our brains that takes the visual input, feeling of muscle tonus, feeling of the force exerted on our body etc. and then gives an answer as to whether we are able to take the next step, pick up a rock and so on. But, mathematicians also want proofs to be useful to explain the nature of the thing in question. Because another thing we want to do about things like picking up rocks, is we want to make that more efficient, make inanimate systems that can pick up rocks etc. ---- NB. I'm not entirely sure how much LLMs can contribute in this field. The first successes of AI were precisely in the field of automated proofs, and that's where symbolic AI seems to work great. But, I'm not at all an expert on LLMs. Maybe there's some way I cannot think about that they would be better at this task, but on the face of it they just aren't.
bumbledraven 2y ago
> as we’ll discuss, it’s a basic metamathematical fact that out of all possible theorems almost none have short proofs Where in the article is this discussed?
- Tainnor 2y ago
  For any possible definition of "short", there's only finitely many (and typically few) theorems that have a short proof, while there are infinitely many theorems (not all of them interesting). More in detail: Proofs are nothing more than strings, and checking the validity of a proof can be done mechanically (and efficiently), so we can just enumerate all valid proofs up to length N and pick out its conclusion.
- optimalsolver 2y ago
  >of all possible theorems almost none have short proofs Ok, but what about the theorems humans would actually care about?
  - Tainnor 2y ago
    We can't really formalise what theorems humans would care about, so I'm afraid this is hard to answer rigorously. But there are some theorems many people care about and they don't have any known short proofs (e.g. Fermat's Last Theorem).
coonjecture 2y ago
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). Automatic formal proofs can be useful when you are able to test [1] https://doi.org/10.1016/j.jpaa.2008.11.043 https://doi.org/10.1016/j.jpaa.2008.11.043 [2] https://ceur-ws.org/Vol-3455/short4.pdf https://ceur-ws.org/Vol-3455/short4.pdf
- supernewton 2y ago
  The thing you're missing is that at no point is it assumed that there are exactly two elements in a boolean algebra. In fact you can have a boolean algebra with four elements (see https://en.wikipedia.org/wiki/Boolean_algebra_(structure) https://en.wikipedia.org/wiki/Boolean_algebra_(structure)).
  - coonjecture 2y ago
    It seems the author is using the word logic, so logic boolean algebra suggests the classical case. Perhaps what is not trivial is that one can use that rule to deduce the other axioms. So that is not the theorem what is important but that one can prove any tautology using that simple axiom.
- mb7733 2y ago
  If I understand you correctly, you're misreading the theorem. The problem isn't to prove that statement, it's to show that if you assume that statement to be true, you get all of boolean logic.
User23 2y ago
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).
- bwfan123 2y ago
  Can you share a good reference to peirce's work on existential graphs ? also, can you share references to how Peano relates to Peirce's work. I loved Peirce's essays, but have not tried to read his work on logic or semiotics.
  - User23 2y ago
    John Sowa is a good resource. Here is his annotation of Peirce's tutorial[1]. Another paper explores the influence of EG on Sowa's Conceptual Graphs[2]. I happen to find the juxtaposition of Frege's notation with Peirce's interesting. Sowa's commentary on yet another Peirce manuscript has some fun historical tidbits about the influence of Peirce on the design of SQL[3]. Here is another reference that mentions Peano's adoption of Peirce's notation[4]. That should be plenty to get you started! Digging through the references in those papers and the bibliography on Sowa's site will find you plenty more modern Peirce scholarship. I think Peirce would be pleased that his seemingly abstract approach to logic ended up inspiring one of the most pragmatically useful classes of software ever, the relational database. [1] https://www.jfsowa.com/pubs/egtut.pdf https://www.jfsowa.com/pubs/egtut.pdf [2] https://www.jfsowa.com/pubs/eg2cg.pdf https://www.jfsowa.com/pubs/eg2cg.pdf [3] https://www.jfsowa.com/peirce/csp1885.HTM https://www.jfsowa.com/peirce/csp1885.HTM [4] https://www.jfsowa.com/pubs/csp21st.pdf https://www.jfsowa.com/pubs/csp21st.pdf
    - bwfan123 2y ago
      thanks !
graycat 2y ago
In proofs in math, there is the old: "Elegance is directly proportional to what you can see in it and inversely proportional to the effort it takes to see it."
sega_sai 2y ago
I have not fully read the whole page, but I wonder if this type of tree of expressions leading to a proof can be explored efficiently with the same idea as Monte-Carlo Tree Search in chess. I.e. surely you can explore all the possible combinations of existing axioms/lemmas, but if you have something like NN, it can suggest the most interested branches of the tree, so you can go deeper in the tree/graph without exponential effort.
deleted 2y ago
[deleted]
unkulunkulu 2y ago
In the bisubstitution example, I cannot see the difference between the source lemma and the target lemma. It looks like A=>A proof. Am I blind?
philzook 2y ago
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/ 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/ 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 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/software/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.
ogogmad 2y ago
It's probably nothing, but one of the pivotal lemmas is (a|(a|(a|b))) = (a|b). Imagine replacing (a|b) with x to get (a|(a|x)) = x; then this identity can be read as "x reflected through 'a' twice gives x". It reminds me of O Loos's axiomatic approach to Symmetric Spaces where the operation | means reflect. It axioms are (x|x) = x; (x|(x|y)) = y; (x|(y|z)) = ((x|y)|(x|z)); and finally that "|" should be a smooth function over some manifold. But then again, when "|" is NAND, it follows that (a|b)|(a|b) means NOT (a|b), which breaks the apparent link to symmetric spaces, because x reflected through itself should give back x.
UltraSane 2y ago
I like the idea of having all known proofs someday formalized in something like Lean so that you could verify all of mathematics with one click. Each new proof would have to be consistent with all other proofs.
daxfohl 2y ago
Is it "just" a problem of a few missing definitions? It reminds me of like a class that has a hundred fields and subfields and lambda types that each have their own hundreds of fields and subfields and lambda types, etc. Typically you can pull out those things, give them a name and independent existence, and the whole thing makes more sense when complete.
deleted 2y ago
[deleted]
deleted 2y ago
[deleted]
swwolfeam 2y ago
Regrettably this guy remains as toxic and polarizing as ever. It was known that the shortest proof possible is a 2 step version of the entire proof. This was publicly pointed out in the past, but this guy removed traces of it. Now he posts this fact as a tiny footnote mark in his 5000 word blog post. Best to avoid giving him HN as platform for self promotion

190 points by ColinWright 2y ago

cbm-vic-20 2y ago

[flagged]

deleted 2y ago
[deleted]

francasso 2y ago

Is there a relation between the "single axiom for boolean algebra" that Wolfram claims to have discovered and the fact that you can express all boolean operations with just NAND?

ur-whale 2y ago
> Is there a relation between the "single axiom for boolean algebra" that Wolfram claims to have discovered and the fact that you can express all boolean operations with just NAND? Seems to be partially answered in the article. Search for "Is There a Better Notation?"
markisus 2y ago
I was sort of puzzled by the meaning of "axiom for boolean algebra" as well, and I looked into this more. The way I learned boolean algebra was by associating certain operations (AND, NOT, OR, etc) to truth tables. In this framework, proving a theorem of boolean algebra would just involve enumerating all possible truth assignments to each variable and computing that the equation holds. There is another framework for boolean algebra that does not involve truth tables. This is the axiomatic approach [1]. It puts forth a set of axioms (eg "a OR b = b OR a"). The symbol "OR" is not imbued with any special meaning except that it satisfies the specified axioms. These axioms, taken as a whole, implicitly define each operator. It then becomes possible to prove what the truth tables of each operator must be. One can ask how many axioms are needed to pin down the truth table for NAND. As you know, this is enough to characterize boolean algebra, since we can define all other operators in terms of NAND. It turns out only one axiom is needed. It is unclear to me whether this was first discovered by Wolfram, or the team of William McCune, Branden Fitelson, and Larry Wos. [2] [1] https://en.wikipedia.org/wiki/Boolean_algebra_(structure) https://en.wikipedia.org/wiki/Boolean_algebra_(structure) [2] https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_algebra#:~:text=In%20mathematical%20logic%2C%20minimal%20axioms https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_alg...,.
- jarpschope 2y ago
  Thanks for the wonderful explanation brother!
- rramadass 2y ago
  Nice comment explaining the difference between two viewpoints. The former one is set theoretic i.e. set of objects (eg. terms) and operations (eg. and/or/not) defined on those objects. The latter is an algebraic specification where a number of properties (expressed by logical formulas which can be axioms or theorems) are expected to be satisfied by the operations. Also see https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_algebra https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_alg... PS: I would take any claim by Stephen Wolfram as having been "the first" to discover anything with a boatload of salt.
Tainnor 2y ago
The latter is a necessary, but not sufficient condition for the former.

ur-whale 2y ago

Here's a meta question about this article: let's try to estimate how many people on earth, say within the next 5 years will ever read the entire article in all of its gory details? These days, an LLM will, perhaps. An make it palatable to puny humans.

deleted 2y ago
[deleted]
philipwhiuk 2y ago
Or maybe it will fail to recall all of it and make something up. Because it has 300B parameters not infinitely many. We currently pull out our phones at the pub/table to check something someone makes up to see if it's legitimate. Now we've invented the technology to have something be that thing that creates a half-truth from what it has absorbed.
astrange 2y ago
Just train the LLM search engine to tell people it contains the answers to all their questions.
queuebert 2y ago
I probably could, but I'm 99% sure it's a thinly veiled self promotion, as is usual from him.

cjfd 2y ago

What is this central dot? I thought a central dot in boolean logic means logical and but then the axiom is clearly false..... I don't get what this is about.

ur-whale 2y ago
> What is this central dot? Yeah, I wish he had started by defining that. The is hard to understand without it. Search for "Is There a Better Notation?" in the article, it seems "." is NAND
- hulium 2y ago
  Technically, his axiom is the definition for what the operator is. Any set together with an operator "•" that satisfies this law is a boolean algebra. Binary logic where •=NAND is one such example because it satisfies the axiom.
- NooneAtAll3 2y ago
  it's simply "Generic Operator". The only requirements is to follow axioms for all its input values. NAND isn't THE operator, it is AN operator that can be in that place. If there's only 1 value that variables can be - "I", then "I \dot I = I" would be a valid operator that follows given axioms
larschdk 2y ago
The source uses ○, not •, for the NAND operation.
BetterWhisper 2y ago
In "The proof as we know" section he states that the dot is a NAND operation Quote: "the · dot here can be thought of as representing the Nand operation"
Tainnor 2y ago
As others have already said, think of it as NAND, although in traditional logic this is typically called the "Sheffer stroke".

robertkoss 2y ago

As someone who is completely unrelated to the academic world, is Stephen Wolfram actually working on meaningful things? I remember reading an article where he was announcing his Physics Project which got a lot of backlash from the scientific community (at least I think that was the case). Nonetheless, every time I browse through Wolfram Alpha I am thoroughly impressed of what it can do with only Natural Language as an input.

meltyness 2y ago
They've got a YouTube with pretty robust updates. Iirc, during the lock downs, he'd do live coding and stuff.
deleted 2y ago
[deleted]
pvg 2y ago
https://hn.algolia.com/?dateRange=all&page=0&prefix=false&query=by%3Adang%20wolfram%20derangement&sort=byDate&type=comment https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
- Tainnor 2y ago
  That's weird, why does Stephen Wolfram gets some sort of special treatment here that nobody else seems to get - including people that are subject to much more common and intense criticism (just the other day there were people bitching about Trudeau, for example - or let's take Elon Musk who is an asshat (IMHO, YMMV), is discussing that off-topic when it comes to how he manages Twitter?). The question "is Stephen Wolfram being taken seriously by the mathematics community?" seems relevant as a question to gauge whether one should spend time reading a very long article. edit: an even more relevant analogy - is Mochizuki's big ego irrelevant in a discussion about whether his proof of the abc conjecture, that nobody understands and which he refuses to explain properly, is correct?
  - pvg 2y ago
    Because it's highly repetitive and uninteresting, especially in the context of an article that is not about Wolfram. The mod exhortations are a consequence of the repetitiveness rather than some special carveout. Other things that get that repetitive get similar appeals.

bmc7505 2y ago

Although Wolfram doesn't mention it by name, this is closely related to what he is trying to do: https://en.wikipedia.org/wiki/Reverse_mathematics https://en.wikipedia.org/wiki/Reverse_mathematics

deleted 2y ago
[deleted]
vasco 2y ago
Wanted to thank you for the share, added "Reverse Mathematics: Proofs from the Inside Out" to my reading list which was referenced in the article you posted: https://www.goodreads.com/book/show/34928283-reverse-mathematics https://www.goodreads.com/book/show/34928283-reverse-mathema...
- bmc7505 2y ago
  Depending on how comfortable you are with model theory you might also enjoy Dzhafarov and Mummert’s textbook, which first brought the subject to my attention.

sylware 2y ago

Formal proof is so much important, since currently maths is built on set theory, I wonder how the set theory axioms are written in some of the formal solvers.

robinzfc 2y ago
No need to wonder for long, just have a look. Metamath: https://us.metamath.org/mpeuni/mmset.html#axioms https://us.metamath.org/mpeuni/mmset.html#axioms Isabelle/ZF: https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html
gaogao 2y ago
You can model types as a set and sets as types in many ways, so a number of the basic set theory axioms are pretty simple to express as lemmas from type axioms. IIRC you get constructive set theory easy, but do have to define additional axioms typically for ZFC.
- JonChesterfield 2y ago
  The C part of ZFC is a challenge for constructive theories
  - sylware 2y ago
    I recall that you really need the "C" from ZFC or you'll end-up with a much less comfy realm of mathematics. So the "C" from ZFC is "challenging" for type theory? Because, and I think I am not that much overshooting, fundamental axioms are really, really simple, even the "C" from ZFC, and if is "challenging" to express it using some fundamental theory, well, not good omens for that theory, or they can rebuild the realm of classic maths with their own "C"??
    - JonChesterfield 2y ago
      The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world of ZFC. I expect there's an equivalent addition to constructive type theory that yields non-constructive type theory. Adding more axioms isn't necessarily making systems better though.

deleted 2y ago

[deleted]

agentultra 2y ago

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?

Davidbrcz 2y ago
It depends. A proven conjecture is IMO better than an unproven one. But usually, a new proof would shed new lights or build bridges between concepts that were before unrelated. And in that sense, a proof not understandable by humans is disappointing, because it doesn't really fullfil the need to understand the reason behind why it's true.
crabbone 2y ago
This isn't a new conundrum. This was a very contentious question in the end of the 19th century, where French mathematicians clashed with the German mathematicians. Poincare is known for describing proofs as texts intended to convince other mathematicians that something is the case, whereas Hilbert believed that automation is the way to go (i.e. have a "proof machine", plug in the question, get the answer and be done with it). Temporarily, Germans won. Personally, I don't think that proofs that cannot be understood have no value. We rely on such proofs all the time in our day-to-day interpretation of the world around us, our ability to navigate it and anticipate it. I.e. there's some sort of an automated proof tool in our brains that takes the visual input, feeling of muscle tonus, feeling of the force exerted on our body etc. and then gives an answer as to whether we are able to take the next step, pick up a rock and so on. But, mathematicians also want proofs to be useful to explain the nature of the thing in question. Because another thing we want to do about things like picking up rocks, is we want to make that more efficient, make inanimate systems that can pick up rocks etc. ---- NB. I'm not entirely sure how much LLMs can contribute in this field. The first successes of AI were precisely in the field of automated proofs, and that's where symbolic AI seems to work great. But, I'm not at all an expert on LLMs. Maybe there's some way I cannot think about that they would be better at this task, but on the face of it they just aren't.

bumbledraven 2y ago

> as we’ll discuss, it’s a basic metamathematical fact that out of all possible theorems almost none have short proofs Where in the article is this discussed?

Tainnor 2y ago
For any possible definition of "short", there's only finitely many (and typically few) theorems that have a short proof, while there are infinitely many theorems (not all of them interesting). More in detail: Proofs are nothing more than strings, and checking the validity of a proof can be done mechanically (and efficiently), so we can just enumerate all valid proofs up to length N and pick out its conclusion.
optimalsolver 2y ago
>of all possible theorems almost none have short proofs Ok, but what about the theorems humans would actually care about?
- Tainnor 2y ago
  We can't really formalise what theorems humans would care about, so I'm afraid this is hard to answer rigorously. But there are some theorems many people care about and they don't have any known short proofs (e.g. Fermat's Last Theorem).

coonjecture 2y ago

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). Automatic formal proofs can be useful when you are able to test [1] https://doi.org/10.1016/j.jpaa.2008.11.043 https://doi.org/10.1016/j.jpaa.2008.11.043 [2] https://ceur-ws.org/Vol-3455/short4.pdf https://ceur-ws.org/Vol-3455/short4.pdf

supernewton 2y ago
The thing you're missing is that at no point is it assumed that there are exactly two elements in a boolean algebra. In fact you can have a boolean algebra with four elements (see https://en.wikipedia.org/wiki/Boolean_algebra_(structure) https://en.wikipedia.org/wiki/Boolean_algebra_(structure)).
- coonjecture 2y ago
  It seems the author is using the word logic, so logic boolean algebra suggests the classical case. Perhaps what is not trivial is that one can use that rule to deduce the other axioms. So that is not the theorem what is important but that one can prove any tautology using that simple axiom.
mb7733 2y ago
If I understand you correctly, you're misreading the theorem. The problem isn't to prove that statement, it's to show that if you assume that statement to be true, you get all of boolean logic.

User23 2y ago

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).

bwfan123 2y ago
Can you share a good reference to peirce's work on existential graphs ? also, can you share references to how Peano relates to Peirce's work. I loved Peirce's essays, but have not tried to read his work on logic or semiotics.
- User23 2y ago
  John Sowa is a good resource. Here is his annotation of Peirce's tutorial[1]. Another paper explores the influence of EG on Sowa's Conceptual Graphs[2]. I happen to find the juxtaposition of Frege's notation with Peirce's interesting. Sowa's commentary on yet another Peirce manuscript has some fun historical tidbits about the influence of Peirce on the design of SQL[3]. Here is another reference that mentions Peano's adoption of Peirce's notation[4]. That should be plenty to get you started! Digging through the references in those papers and the bibliography on Sowa's site will find you plenty more modern Peirce scholarship. I think Peirce would be pleased that his seemingly abstract approach to logic ended up inspiring one of the most pragmatically useful classes of software ever, the relational database. [1] https://www.jfsowa.com/pubs/egtut.pdf https://www.jfsowa.com/pubs/egtut.pdf [2] https://www.jfsowa.com/pubs/eg2cg.pdf https://www.jfsowa.com/pubs/eg2cg.pdf [3] https://www.jfsowa.com/peirce/csp1885.HTM https://www.jfsowa.com/peirce/csp1885.HTM [4] https://www.jfsowa.com/pubs/csp21st.pdf https://www.jfsowa.com/pubs/csp21st.pdf
  - bwfan123 2y ago
    thanks !

graycat 2y ago

In proofs in math, there is the old: "Elegance is directly proportional to what you can see in it and inversely proportional to the effort it takes to see it."

sega_sai 2y ago

I have not fully read the whole page, but I wonder if this type of tree of expressions leading to a proof can be explored efficiently with the same idea as Monte-Carlo Tree Search in chess. I.e. surely you can explore all the possible combinations of existing axioms/lemmas, but if you have something like NN, it can suggest the most interested branches of the tree, so you can go deeper in the tree/graph without exponential effort.

deleted 2y ago

[deleted]

unkulunkulu 2y ago

In the bisubstitution example, I cannot see the difference between the source lemma and the target lemma. It looks like A=>A proof. Am I blind?

philzook 2y ago

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/ 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/ 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 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/software/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.

ogogmad 2y ago

It's probably nothing, but one of the pivotal lemmas is (a|(a|(a|b))) = (a|b). Imagine replacing (a|b) with x to get (a|(a|x)) = x; then this identity can be read as "x reflected through 'a' twice gives x". It reminds me of O Loos's axiomatic approach to Symmetric Spaces where the operation | means reflect. It axioms are (x|x) = x; (x|(x|y)) = y; (x|(y|z)) = ((x|y)|(x|z)); and finally that "|" should be a smooth function over some manifold. But then again, when "|" is NAND, it follows that (a|b)|(a|b) means NOT (a|b), which breaks the apparent link to symmetric spaces, because x reflected through itself should give back x.

UltraSane 2y ago

I like the idea of having all known proofs someday formalized in something like Lean so that you could verify all of mathematics with one click. Each new proof would have to be consistent with all other proofs.

daxfohl 2y ago

Is it "just" a problem of a few missing definitions? It reminds me of like a class that has a hundred fields and subfields and lambda types that each have their own hundreds of fields and subfields and lambda types, etc. Typically you can pull out those things, give them a name and independent existence, and the whole thing makes more sense when complete.

deleted 2y ago

[deleted]

deleted 2y ago

[deleted]

swwolfeam 2y ago

Regrettably this guy remains as toxic and polarizing as ever. It was known that the shortest proof possible is a 2 step version of the entire proof. This was publicly pointed out in the past, but this guy removed traces of it. Now he posts this fact as a tiny footnote mark in his 5000 word blog post. Best to avoid giving him HN as platform for self promotion