[HN Gopher] Who Can Understand the Proof? A Window on Formalized...
___________________________________________________________________
Who Can Understand the Proof? A Window on Formalized Mathematics
Author : ColinWright
Score : 162 points
Date : 2025-01-10 12:21 UTC (10 hours ago)
(HTM) web link (writings.stephenwolfram.com)
(TXT) w3m dump (writings.stephenwolfram.com)
| francasso wrote:
| 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 wrote:
| > 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 wrote:
| 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)
|
| [2] https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_al
| g...,.
| jarpschope wrote:
| Thanks for the wonderful explanation brother!
| rramadass wrote:
| 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_Boo
| lean_alg...
|
| PS: I would take any claim by Stephen Wolfram as having been
| "the first" to discover anything with a boatload of salt.
| Tainnor wrote:
| The latter is a necessary, but not sufficient condition for the
| former.
| ur-whale wrote:
| 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.
| philipwhiuk wrote:
| 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 wrote:
| Just train the LLM search engine to tell people it contains the
| answers to all their questions.
| queuebert wrote:
| I probably could, but I'm 99% sure it's a thinly veiled self
| promotion, as is usual from him.
| cjfd wrote:
| 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 wrote:
| > 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 wrote:
| 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 wrote:
| 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 wrote:
| The source uses *, not *, for the NAND operation.
| BetterWhisper wrote:
| 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 wrote:
| As others have already said, think of it as NAND, although in
| traditional logic this is typically called the "Sheffer
| stroke".
| etwas wrote:
| The dot is not simply NAND or NOR.
|
| Search for "What Actually Is the "*"?" for the answer, it's
| quite complex and fascinating.
| bo1024 wrote:
| I was not able to find anything, can you help with locating
| what you're talking about?
| NooneAtAll3 wrote:
| the whole point of this discipline is that this dot is simply a
| "generic Operator"
|
| you can use whatever symbol you want
|
| all you really know - is the axiom you're given, which
| transforms one tree structure of operator application into a
| different one
|
| NAND suggested in replies isn't THE operator, it's AN operator
| that follows given rules
| robertkoss wrote:
| 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 wrote:
| They've got a YouTube with pretty robust updates. Iirc, during
| the lock downs, he'd do live coding and stuff.
| pvg wrote:
| https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
| Tainnor wrote:
| 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 wrote:
| 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.
| Tainnor wrote:
| 90% of content on HN is repetitive. "Unit tests suck",
| "managers forcing return to the office are assholes",
| "Fauci lied about Covid", ...
|
| I've never seen a single of these things being called
| out.
|
| This is an article about a proof Stephen Wolfram claims
| to have discovered. Somebody further upthread already
| mentioned that this may not actually be true, or that the
| credit at least should be shared.
| pvg wrote:
| 90% of everything is repetitive. The generic analogies
| method is not really that useful in discussing the
| specific thing you asked about.
|
| _I 've never seen a single of these things being called
| out._
|
| Happens all the time plus many repetitive things
| constantly get moderated away by users and moderators.
| The goal is a less boring messageboard, but it's
| aspirational rather than perfectly achievable.
|
| Edit: Ok, fine, let's do analogies. Imagine Elon Musk
| started writing long, interesting, researched articles
| about some topic, say, Chinese history. If every such
| article got flooded with discussions about who does and
| does not like Elon Musk and by how much, those would
| start getting modbleatings too. This is what happened
| except it wasn't Elon Musk but Stephen Wolfram and it
| wasn't Chinese History and it started about a decade ago
| (as you can see from the comment dates).
| Tainnor wrote:
| Maybe the reason why people keep calling out Stephen
| Wolfram (and have been doing so for a decade) is because
| he has a history of making grandiose claims that do not
| always withstand closer scrutiny?
|
| I'm not claiming that Stephen Wolfram is an idiot or that
| nothing he writes is of value, but his ego clearly does
| influence his judgement so it makes no sense to me to
| claim that it is off-topic (in the way that, say, his
| love life or his opinion on abortion would be).
|
| Also this:
|
| > Happens all the time plus many repetitive things
| constantly get moderated away by users and moderators.
| The goal is a less boring messageboard, but it's
| aspirational rather than perfectly achievable.
|
| No sorry, I've been on HN during the pandemic and I was
| this close to quitting it forever. These things do _not_
| get called out in any consistent fashion for many topics.
| I 'm pretty sure a message board for people interested in
| technology can handle a couple of "Wolfram sucks"
| comments a year better than literally hundreds of angry
| rants about a health advisor that doesn't even have any
| relevance to anyone who isn't from the US.
| pvg wrote:
| _Maybe the reason why people keep calling out_
|
| It's not about the reason, it's about the repetitiveness.
| The boringness of the repetitiveness is one of the
| organizing principles of HN. Also, people don't actually
| 'keep calling out' this stuff - these moderator
| interventions, specifically in the Wolfram case, have
| been surprisingly effective. Many Wolfram-y articles have
| neither moderation intervention or bad tangents.
|
| _These things do not get called out in any consistent
| fashion for many topics._
|
| You don't see everything, neither do other forum
| participants, including the moderators. The fact that,
| collectively, some boring and repetitive stuff is missed
| doesn't imply we can all use more boring, repetitive
| stuff.
| Tainnor wrote:
| > You don't see everything, neither do other forum
| participants, including the moderators.
|
| The stuff that I mentioned was really hard to miss.
|
| The question OP asked was, essentially, "is Stephen
| Wolfram actively contributing to the mathematical
| community?". If you really think that this is off-topic
| then... I don't know what to say.
| queuebert wrote:
| Wolfram is essentially the Fauci of physics.
| mr_mitm wrote:
| No. Even though Mathematica is arguably meaningful. It's very
| popular with some scientists, and in many aspects it's a
| respectable piece of software.
|
| A few years ago Sean Carroll was hosting him on his podcast. It
| was a bit surprising to me because Sean would never give a
| crackpot the time of the day, and Wolfram is borderline in
| crackpot territory IMHO, but not quite. He hasn't published
| anything meaningful in a scientific journal in a long time as
| far as I know.
| ericbarrett wrote:
| I am neither a mathematician nor a scientist, so I'm
| unqualified to judge Wolfram's current theories* of physics
| and computation. But my impression is that he remains quite
| rigorous in his work, even if the path he's walking is far
| from the main. And of course he's quite bombastic, which
| always seems to raise hackles. In fact, the article on which
| this discussion anchors is a great example of both.
|
| * Ref: https://www.wolframphysics.org/technical-introduction/
| The podcast with Sean Carroll that parent mentioned is also a
| surprisingly accessible lay introduction, definitely worth a
| listen.
| empath75 wrote:
| As far as I can tell, he's not a crackpot, and doesn't say
| anything that isn't _true_, he just wastes a lot of time
| going down dead ends, and relentlessly promotes himself.
|
| Like all the stuff about Rule 30 that he writes _endlessly_
| about is both true and about 1/100th as interesting as he
| evidently thinks it is.
| jlouis wrote:
| Define "meaningful".
|
| A lot of mathematics is about exploration. You look at some
| system and try to figure out how it works. If you have a good
| idea (conjecture), you try proving or disproving it. The goal
| is to gain some understanding.
|
| Once in a while, it turns out that exploration hits the gold
| ore in the mine. You get something that applies to solving some
| problem we've had for years. As an example, algebra was
| considered meaningless for years. Then cryptography came along.
|
| There are other good examples. Reed-Solomon coding relies on a
| basis of finite fields.
|
| The problem is we don't really know when we'll strike gold in
| many cases. So people go exploring. It also involves humans,
| and they can disagree on a lot of things. Stephen seems to run
| into disagreements more often than the average researcher, at
| least historically.
| pepinator wrote:
| Has he gained interesting understanding of anything?
| j16sdiz wrote:
| He is trying to do alternative theory of science.
|
| It's like rewriting (and clarifying things here or there,
| putting in new analogies, etc.. not just translating)
| everything in Klingon, and creating new Klingon words while he
| is doing that.
|
| Sure this is "interesting" in academic sense. Good luck finding
| a journal accept paper written in Klingon.
| the__alchemist wrote:
| His physics project is high risk, and probably wrong. But very
| worth it. He's working on things outside what the physics
| community is focused on. And there are incentives for them to
| keep working the same angles. IMO you need outsiders to spark
| progress in cases like this. I will continue reading his work
| and progress.
|
| I think, specifically, his vision is very different and radical
| from other things I've seen, which you'd think would lend
| itself to at least one currently-testable hypothesis, but I
| haven't seen one. It seems there may overfitting. He has a way
| for every major principle in physics to fit into his theory,
| but no _new_ ones, or flaws in current ones; that 's what
| worries me. I hope he continues working on it. (Unlikely he'll
| stop after this many decades)
|
| As a comparison, I'm more hopeful for this than String theory,
| and the latter has been found worthy of physicist's time, so I
| certainly think this is.
|
| Regarding the _crackpot_ angle: I think that is not an
| appropriate label: If you look at the people that the label
| canonically applies to, you will find people who have no idea
| what they 're talking about, who don't understanding the math
| and physics etc. That is not the case here; he knows it as well
| as anyone.
| bmc7505 wrote:
| 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
| vasco wrote:
| 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-mathema...
| bmc7505 wrote:
| 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 wrote:
| 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 wrote:
| No need to wonder for long, just have a look.
|
| Metamath: https://us.metamath.org/mpeuni/mmset.html#axioms
|
| Isabelle/ZF:
| https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html
| gaogao wrote:
| 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.
| luma wrote:
| Check out mathlib for LEAN, the pace of proofs being added here
| is breathtaking: https://github.com/leanprover-
| community/mathlib4
| staunton wrote:
| > currently maths is built on set theory
|
| most mathematicians will eventually agree with that when
| pressed. However, almost none of them know the axioms of ZFC by
| heart (because they don't need them). You can swap out ZFC for
| something else and nobody will care very much as long as "the
| same" (does a lot of work here) theorems, which they know and
| use it their work, remain true.
|
| This is what many theorem provers do. Many aren't based on set
| theory, for example, but instead on type theory. (You can still
| do set theory in a framework based on type theory, and vice
| versa, but the foundations are "different").
| agentultra wrote:
| 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 wrote:
| 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 wrote:
| 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.
| rocqua wrote:
| From what I have heard when talking to the people behind
| formal analysis of protocol security, the main problem
| currently with using LLMs to 'interact with the theorem
| prover for you' is that there is nowhere near enough proofs
| out there for the LLMs to learn how to generalize from them.
| chii wrote:
| i would imagine a proof has several "uses": 1) the proof itself
| is useful for some other result or proof, and 2), the proof is
| using a novel technique or uses novel maths, or links to
| previously unlinked fields, and it's not the proof's result
| itself that is useful, but the technique developed. This
| technique can then be applied in other areas to produce other
| kinds of proofs or knowledge.
|
| I suspect it is the latter that will suffer in automated proofs
| perhaps - without understanding the techniques, or if the
| technique is not really novel but just tedious.
| knappa wrote:
| Mathematician here (trained as pure, working as applied). Non-
| elegant proofs are useful, if the result is important. e.g.
| People would still be excited by an ugly proof of the Riemann
| hypothesis.^1 It's important too a lot of other theorems if
| this is true or not. However, if the result is less central you
| won't get a lot of interest.
|
| Part of it is, I think, that "elegance" is flowery language
| that hides what mathematicians really want: not so much new
| proofs as new proof techniques and frameworks. An "elegant"
| proof can, with some modification, prove a lot more than its
| literal statement. That way, even if you don't care much about
| the specific result, you may still be interested because it can
| be altered to solve a problem you _were_ interested in.
|
| 1: It doesn't have to be as big of a deal as this.
| The_suffocated wrote:
| _" It doesn't have to be as big of a deal as this."_
|
| Agree. The truthfulness of the four-colour theorem is good to
| know, although there is not yet any human-readable proof.
| rocqua wrote:
| I feel like the four-color theorem automated proof is much
| more 'human-readable' than the proofs done with automated
| theorem provers. Because with the four-color theorem, there
| is a human readable proof that says "if this finite set of
| cases are all colorable, then all planar graphs are
| colorable". And then there is some rather concrete code
| that generates all the finite cases, and finds a coloring
| for them. Every step in there makes sense, and is fully
| understandable. The fact that the exhaustive checking
| wasn't done by hand doesn't mean its hard to understand how
| the proof works, or what is 'actually going on'.
|
| For a general theorem prover, reading the code doesn't
| explain anything insightful about why the theorem is true.
| For the 4 color theorem, the code that proved it actually
| gives insight in how the proof works.
| LegionMammal978 wrote:
| Then again, even an 'elegant' proof can be surprisingly
| inflexible. I've recently been working through Apery's proof
| that z(3) is irrational. It's so simple that even a clueless
| dabbler like me can understand all the details. Yet no one
| has been able to make his construction work directly for
| anything else (that hasn't already been proven irrational).
| C'est la vie, I suppose.
| rocqua wrote:
| There was a post yesterday of a quanta article:
| https://news.ycombinator.com/item?id=42644896.
|
| The article explains that two mathematicians were able to
| place Apery's proof that z(3) is irrational into a much
| wider (and hence more powerful) framework. I doubt that
| framework is as easy to understand as the original proof.
| But in the end something with wider applicability did come
| out of the proof.
| LegionMammal978 wrote:
| Yeah, many of the fancy analytic methods are beyond my
| level of dabbling. I've been trying to learn more about
| them, so I can solve the myriad exercises left to the
| reader in all the Diophantine approximation papers.
|
| Still, the newer methods publicized in the Quanta article
| definitely get more involved, and at least from my
| perspective they don't establish things as elegantly as
| Apery's z(2) and z(3) arguments do. Hopefully they turn
| out to be powerful in practice, to make up for it.
| User23 wrote:
| One thing that many mathematicians today don't think about is
| how deeply intertwined the field has historically been with
| theology. This goes back to the Pythagoreans at least.
|
| That survives in the culture of mathematics where we continue
| to see a high regard for truth, beauty, and goodness. Which,
| incidentally, are directly related to logic, aesthetics, and
| ethics.
|
| The value of truth in a proof is most obvious.
|
| The value of aesthetics is harder to explain, but there's no
| denying that it is in fact observably valued by
| mathematicians.
|
| As for ethics, remember that human morality is a proper
| subset thereof. Ethics concerns itself with what is good. It
| may feel like a stretch, but it's perfectly reasonable to say
| that for two equally true proofs of the same thing, the one
| that is more beautiful is also more good. Also, obviously,
| given two equally beautiful proofs, if only one is true then
| it is also more good.
| Xcelerate wrote:
| > That survives in the culture of mathematics where we
| continue to see a high regard for truth, beauty, and
| goodness
|
| As a non-mathematician, I've noticed this as well, and I
| have a suspicion the historical "culture" is holding the
| field back. Godel proved there are an infinite number of
| true arithmetic statements unprovable within any
| (consistent, sufficiently powerful) formal system. But our
| "gold standard" formal system, ZFC, has about as many
| axioms as we have fingers -- why is finding more axioms not
| the absolute highest priority of the field?
|
| We struggle to prove facts about Turing machines with only
| six states, and it's not obvious to me that ZFC is even
| capable of resolving all questions about the behavior of
| six state Turing machines (well, specifically just ZF, as C
| has no bearing on these questions).
|
| Yet Turing machines are about as far from abstract
| mathematics as one can get, because you can actually build
| these things in our physical universe and observe their
| behavior over time (except for the whole "infinite tape"
| part). If we can't predict the behavior of the majority of
| tiny, _deterministic_ systems with ZFC, what does that say
| about our ability to understand and predict real world
| data, particularly considering that this data likely has an
| underlying algorithmic structure vastly more complex than
| that of a six state Turing machine?
|
| More formally, my complaint with the culture of mathematics
| is:
|
| 1) We know that for any string of data, I(data : ZFC) <=
| min(K(data), K(ZFC)) + O(1)
|
| 2) K(ZFC) is likely no more than a few bytes. I think the
| best current upper bound is the description length of a
| Turing machine with a few hundred states, but I suspect the
| true value of K(ZFC) is far lower than that
|
| 3) Thus K(data) - K(data | ZFC) <= "a few bytes"
|
| Consider the massive amounts of data that we collect to
| train LLMs. The totality of modern mathematics can provide
| no more than a few bytes of insight into the "essence" of
| this data (i.e., the maximally compressed version of the
| data). Which directly translates to limited predictability
| of the data via Solomonoff induction. And that's _in
| principle_ -- this doesn 't even consider the amount of
| time involved. If we want to do better, we need more
| axioms, full stop.
|
| One might counter, "well sure, but mathematicians don't
| necessarily care about real world problems". Ok, just apply
| the same argument to the set of all arithmetic truths. Or
| the set of unprovable statements in the language of a
| formal system (that are true within some model). That's
| some interesting data. Surely ZFC can discover most "deep"
| mathematical truths? Not very likely. The deeper truths
| tend to occur at higher levels of the arithmetic hierarchy.
| The higher in the hierarchy, the more interesting the
| statement. And these are _tiny_ statements too: [?]x [?]y
| [?]z [...]. Well we 're already in trouble because ZFC can
| only decide a small fraction of the P_2 statements that can
| fit on a napkin and it drops off very quickly at higher
| levels than that. Again, we need more axioms.
| nyssos wrote:
| > Yet Turing machines are about as far from abstract
| mathematics as one can get, because you can actually
| build these things in our physical universe and observe
| their behavior over time (except for the whole "infinite
| tape" part)
|
| The infinite tape part isn't some minor detail, it's the
| source of all the difficulty. A "finite-tape Turing
| machine" is just a DFA.
| Xcelerate wrote:
| > is just a DFA
|
| Oh is that all? If resource bounded Kolmogorov complexity
| is that simple, we should have solved P vs NP by now!
|
| I debated adding a bunch of disclaimers to that
| parenthetical about when the infinite tape starts to
| matter, but thought, nah, surely that won't be the
| contention of the larger discussion point here haha
| User23 wrote:
| It's an LBA, a Linear Bounded Automata.
| mb7733 wrote:
| > > That survives in the culture of mathematics where we
| continue to see a high regard for truth, beauty, and
| goodness
|
| > As a non-mathematician, I've noticed this as well, and
| I have a suspicion the historical "culture" is holding
| the field back.
|
| Holding the field back from what? If the goal of the
| practitioners of the field is to seek mathematically
| beauty, then well, that is what they will focus on.
|
| Besides that, I don't really follow your argument about
| Godel & information theory & that adding more axioms is
| the key to moving math forwards. In the vast majority of
| cases, the difficulty in finding a proof of a statement
| is not that the statement isn't provable under a given
| formal system, it's that we simply can't find it. But
| maybe I misunderstand you?
| dataflow wrote:
| > Part of it is, I think, that "elegance" is flowery language
| that hides what mathematicians really want: not so much new
| proofs as new proof techniques and frameworks. An "elegant"
| proof can, with some modification, prove a lot more than its
| literal statement. That way, even if you don't care much
| about the specific result, you may still be interested
| because it can be altered to solve a problem you _were_
| interested in.
|
| Do you feel this could be a matter of framing? If you view
| the "proof" as being the theorem prover itself, plus the
| proof that it is correct, plus the assumptions, then whatever
| capability it gains that lets it prove your desired result
| probably _is_ generalizable to other things you were
| interested in. It would seem like a loss if they 're
| dismissed simply because their scratch work is inscrutible.
| QuesnayJr wrote:
| I think mathematicians want something more basic, though
| elegance and simplicity are appreciated. They want to know
| _why_ something is true, in a way that they can understand.
| People will write new proof of existing results if they think
| they get at the "why" better, or even collect multiple proofs
| of the same result if they each get at the "why" in different
| ways.
| agentultra wrote:
| In my limited experience it seems like the "why" of a proof
| requires a _theory of mind_ from the perspective of the
| author of the proof.
|
| What I mean is that one could choose a particular tactic to
| proving a lemma or even rely on certain lemma where that
| choice is intended for the audience the author has in mind in
| order to help them understand the steps better.
|
| The _context_ an LLM uses is limited (though growing).
| However its context is lacking the ability to understand the
| mind of the interlocutor and the proof they would expect or
| find helpful.
|
| "Why this proof?" also has a more _global_ context as well.
| It seems there are have been styles and shifts in cultural
| norms over the years in proofs. Even though the Elements
| stood up until the 19th century we don 't necessarily write
| proofs in the style of Euclid even though we may refer to
| those themes and styles, on purpose, in order to communicate
| a subtle point.
| flatline wrote:
| Hypothesis: an LLM capable of generating a correct proof in a
| formal language, not through random chance but through whatever
| passes for "reasoning," should also be capable of describing
| the proof in a way meaningful to humans. Because LLMs have a
| limited context window and are trained on human behavior, they
| will generate solutions similar to what humans would generate.
|
| We have already accepted some proofs we cannot fully
| understand, such as the proof of the four color theorem that
| used computational methods to explore a large solution space
| and demonstrate that no possible special-case combinations
| violate the theorem. But that was just one part of the proof.
|
| I wonder what we know about proof space generally, and if we
| had an ASI that reasoned in a substantially different way than
| humans, what types of proofs it would be likely to generate. Do
| most proofs contain structural components that humans find
| pleasing? Do most devolve into convoluted case analyses? Is
| there a simplest form that a set of correct proofs could be
| reduced to?
| ndriscoll wrote:
| To me this seems obvious. Copilot might generate _wrong_
| things, but what I 've seen tends to be human-readable. My
| experience with Lean is that it feels very much like a
| functional programming language like Scala, so I'd have to
| assume that a coding assistant that also knows Lean
| syntax/libraries would work just like any other programming
| language.
|
| There will perhaps need to be a transition period where we
| might need to look at basic type theory augmenting or
| replacing material in introductory proof classes. Instead of
| truth tables and ZFC, teach math-as-programming. Propositions
| are types, implications are functions, etc. If you have the
| right foundation, I think the stuff ends up being quite
| legible. Mathlib is very abstract which makes it harder to
| approach as a beginner, but you could imagine a sort of
| literate programming approach where we walk students through
| building their own personal Mathlib, refactoring it to use
| higher abstractions as they build it up, etc. In a sense this
| is what a math education is today, but with a kind of half-
| formal, half-natural language and with a bunch of implicit
| assumptions about what techniques the student really knows
| (since details are generally omitted) vs. letting them use
| whatever macros/tactics/theorems they've learned/created in
| other courses.
|
| This could all be especially powerful if the objects you're
| working with have good Widgets[0][1] so you could visualize
| and interact with various intermediate expressions. I see
| tons of potential here. The Lean games[2] also show the
| potential for a bright future here that's kind of along the
| lines of "build your own library around topic X" (the NN game
| has been posted here a few times, but it's actually a
| framework with other games too!).
|
| [0] https://lean-
| lang.org/lean4/doc/examples/widgets.lean.html
|
| [1] https://github.com/leanprover-
| community/ProofWidgets4/blob/m...
|
| [2] https://adam.math.hhu.de/
| math-ias wrote:
| I believe knowing a proof exists will bring us closer to
| elegant human proofs.
|
| I wanted to justify this with the "Roger Bannister Effect". The
| thought is that we're held back psychologically by the idea of
| the impossible. It takes one person to do it. And now everyone
| can do it, freed from the mind trap. But further reading shows
| we were incrementally approaching what Roger Bannister did
| first: the 4 minute mile. And the pause before that record was
| likely not psychological but physical with World War Two. [0]
| And this jives with the TFA when Mr. Wolfram writes about a
| quarter of a century not yielding a human interpretation of his
| computer's output.
|
| All I'm left with is my anecdotes. I had a math professor in
| college who assigned homework every class. Since it was his
| first time teaching, he came up with the questions live. I'd
| come to class red in the face after struggling with questions
| all night. Then the professor would sheepishly reveal some of
| his statements were false. That unknown sapped a lot of
| motivation. Dead ends felt more conclusive. Falsehood was an
| easy scapegoat.
|
| [0] https://www.scienceofrunning.com/2017/05/the-roger-
| bannister...
| QuesnayJr wrote:
| I think there is something to this idea. There have been
| cases where person A was working on proving a result but
| struggled, then person B announced a proof of the result, and
| then person A was inspired to finish their proof. (Sadly, I
| don't remember the specifics.)
| glenstein wrote:
| >One of the perennial questions about proof automation has been
| the utility of proofs that cannot be understood by humans.
|
| I'm skeptical of an in-principle impossibility of understanding
| complex proofs. I think computers likely will have, or already
| do have, a capability for explaining proofs piecemeal, with
| explanations that bridge from the proof itself to familiar
| intuitions.
|
| Needing to understanding by increasingly sophisticated bridge
| explanations may be us getting further removed from immediate
| understanding but I don't think it crosses a magical threshold
| or anything that fundamentally calls into question how
| operational/useful the proofs are.
| youoy wrote:
| An ugly proof is super useful. It turns a statement into a
| theorem.
|
| There is a famous quote by Riemann: "If only I had the
| theorems! Then I should find the proofs easily enough. "
|
| Once you have a proof, simplifying it should be much easier,
| even for computers.
| bumbledraven wrote:
| > 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 wrote:
| 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 wrote:
| >of all possible theorems almost none have short proofs
|
| Ok, but what about the theorems humans would actually care
| about?
| coonjecture wrote:
| 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 [2] https://ceur-
| ws.org/Vol-3455/short4.pdf
| supernewton wrote:
| 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)).
| coonjecture wrote:
| 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.
| User23 wrote:
| 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 wrote:
| 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 wrote:
| 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
|
| [2] https://www.jfsowa.com/pubs/eg2cg.pdf
|
| [3] https://www.jfsowa.com/peirce/csp1885.HTM
|
| [4] https://www.jfsowa.com/pubs/csp21st.pdf
| bwfan123 wrote:
| thanks !
| graycat wrote:
| 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 wrote:
| 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.
| unkulunkulu wrote:
| 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 wrote:
| 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.
| ogogmad wrote:
| 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.
___________________________________________________________________
(page generated 2025-01-10 23:00 UTC)