hckrnws

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?

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.

Then again, even an 'elegant' proof can be surprisingly inflexible. I've recently been working through Apéry's proof that ζ(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.

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 ζ(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.

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 Apéry's ζ(2) and ζ(3) arguments do. Hopefully they turn out to be powerful in practice, to make up for it.

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.

> 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. Gödel 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 Π_2 statements that can fit on a napkin and it drops off very quickly at higher levels than that. Again, we need more axioms.

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

> 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

It’s an LBA, a Linear Bounded Automata.

No, an LBA in general doesn't have a finite tape. It still has an infinite tape, to accommodate arbitrary length inputs, it's just that the tape cannot grow beyond the length of its input (or a constant multiple of it, which is equivalent by the linear speedup trick).

Arbitrarily long and infinite are very different things.

No, they're not.

The point is that a finite tape isn't enough for an LBA.

No they really are. Arbitrarily long means "pick a number any number." Infinite means, well infinite. And infinity is always bigger than "pick a number, any number."

I suggest that you read Michael Sipser's Introduction to the Theory of Computation. It's absolutely lovely and an easy read, considering the subject matter. It will help you to understand cardinality (and many other things) in a pragmatic computing science context.

It may be surprising to you that I've actually read a good portion of that text as well as other books on the subject. Or that I actually do understand what a cardinality is in a "pragmatic computing science context" (whatever that's supposed to mean).

> Infinite means, well infinite

There's a technical definition of "infinite cardinality" which is a bit more rigorous than "well infinite". If |S| > n for every natural number n, then S has infinite cardinality basically by definition.

Why don't you try implementing an LBA simulator in your favourite programming language with a finite-sized array and tell me how it goes? Anyway, the original point was that a Turing Machine with a finite tape is an FSM. This is true (well, or more technically: it's equivalent to an FSM) because you can encode all possible configurations of the tape with a finite set of states and thus don't need any extra memory.

> > 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?

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

Holding the field back from answering questions about the behavior of simple deterministic systems that arguably have an outsized influence on science, machine learning, and mathematics itself. I don't disagree that "beauty" is certainly subjective, but the mathematics research that gets funded by universities and research labs is only tangentially related to such an aesthetic notion.

> 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

Finding a proof is an inherently algorithmic process. Presumably, the human brain uses heuristics (intuition) that have thus far managed to beat simple algorithmic approaches. But it's hard to believe that's going to last much longer. As an extreme example, simply knowing more values of the Busy Beaver function allows one to find proofs more easily. For example, encode the veracity of the statement corresponding to Fermat's Last Theorem into a program (a k-state Turing machine) that dovetails enumeration over all possible values for x, y, z, and n > 2. This program halts if the statement is satisfied by some set of natural numbers and never halts otherwise. But if we know which k-state Turing machine corresponds to BB(k), then we just run the two programs in parallel and if the Fermat program hasn't halted by the time the program for BB(k) has, then the conjecture is true (necessarily false otherwise). Scott Aaronson has written some articles and blog posts about this.

Now the argument I'm making doesn't necessarily depend on trying to determine more values of the uncomputable busy beaver function. You don't have to know the fastest growing computable sequence in order to derive some benefit from greater knowledge of the halting sequence. If we presume that an interesting proof exists within ZFC, then more axioms (that constitute a more powerful system) can lead to much shorter proofs. This is a result obtained from the work of Gödel, Feferman, Jean-Yves Girard, et al. So while you're right that a conjecture we are interested in might have a proof that "exists" within ZFC, whether the minimal such proof can be written down in a human lifespan is a different question. Considering there are many famous conjectures that have been open for centuries now, perhaps the next step isn't having more people stare harder at the problem but rather enriching our foundational formal systems with additional axioms.

I can’t tell if this is crazy or brilliant. Math has been working diligently for a long time to reduce the axioms. Most of the obvious Gödel sentences are stupid things like there is a number that is the proof of itself. The whole project is to derive all of the structure of mathematics, with a high information complexity, from basic axioms but also from comp,ex definitions. I think the definitions (natural numbers as sets, integers as equivalence sets of pairs of natural numbers, etc.) pump up the information complexity from the axioms. Like the initial state of Life allowing arbitrary computation from the simple Life rules.

The idea that there might be more axioms that would let one deduce more about computable complexity classes or the like seems pretty unlikely.

The number of provable statements and unprovable statements is countably infinite and we aren’t lacking the ability to prove things due to obviously true missing axioms.

> 1) We know that for any string of data, I(data : ZFC) ≤ min(K(data), K(ZFC)) + O(1)

What are I and K? What does "data : ZFC" mean?

K(x) is the Kolmogorov complexity of x, i.e., the length of the shortest program that halts and outputs x, typically defined with respect to a universal Turing machine.

I(x : y) = K(x) + K(y) - K(x, y) is the mutual algorithmic information of two strings. It is the algorithmic equivalent to Shannon's mutual information. No algorithm f can increase the mutual algorithmic information between two strings, i.e. ∀f I(x : f(y)) ≤ I(x : y) + O(log(K(f))).

I used "data" to denote any collection of interesting data at all. For example, it could be data obtained from the real world, the observed behavior of Turing machines at very long timescales, or a collection of mathematical proofs. By "ZFC" I just mean the description of any program that enumerates all proofs of ZFC.

The takeaway here is that ZFC is very limited in what it can say about real world data or even what it can say about almost all deterministic computations, including those with very short programs. Levin describes this much better than I could in his famous "Forbidden Information" paper: https://arxiv.org/pdf/cs/0203029.

Levin further argues that extending PA is unlikely... I tend to disagree on that point. How did we get the more powerful theory of ZFC or any of these axioms in the first place then? They are coming from somewhere. But I'm not even going to attempt to debate Levin's case on Hacker News haha

There are plenty of mathematicians - mostly set theorists - who are actively working on finding new axioms of mathematics to resolve questions which can't be resolved by ZFC. Projective Determinacy is probably the most important example of a new axiom of mathematics which goes far beyond what can be proved in ZFC, but which has become widely accepted by the experts. (See [1] for some discussion about the arguments in favor of projective determinacy, and [2] for a taste of Steel's position on the subject.)

I suggest reading Kanamori's book [3] if you want to learn more about this direction. (There are plenty of recent developments in the field which occured after the publication of that book - for an example of cutting edge research into new axioms, see the paper [4] mentioned in one of the answers to [5].)

If you are only interested in arithmetic consequences of the new axioms, and if you feel that consistency statements are not too interesting (even though they can be directly interpreted as statements about whether or not certain Turing machines halt), you should check out some of the research into Laver tables [6], [7], [8], [9]. Harvey Friedman has also put a lot of work into finding concrete connections between advanced set-theoretic axioms and more concrete arithmetic statements, for instance see [10].

[1] https://mathoverflow.net/questions/479079/why-believe-in-the... [2] https://cs.nyu.edu/pipermail/fom/2000-January/003643.html [3] "The Higher Infinite: Large Cardinals in Set Theory from their Beginnings" by Akihiro Kanamori [4] "Large cardinals, structural reflection, and the HOD Conjecture" by Juan P. Aguilera, Joan Bagaria, Philipp Lücke, https://arxiv.org/abs/2411.11568 [5] https://mathoverflow.net/questions/449825/what-is-the-eviden... [6] https://en.wikipedia.org/wiki/Laver_table [7] "On the algebra of elementary embeddings of a rank into itself" by Richard Laver, https://doi.org/10.1006%2Faima.1995.1014 [8] "Critical points in an algebra of elementary embeddings" by Randall Dougherty, https://arxiv.org/abs/math/9205202 [9] "Braids and Self-Distributivity" by Patrick Dehornoy [10] "Issues in the Foundations of Mathematics" by Harvey M. Friedman, https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3137697

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

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

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.

And of course if you come across an inelegant proof you suddenly have the opportunity to think about it and see if you can make it more elegant!

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

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

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.

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.

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.

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.

Though, say we finally solve chess. There's not always going to be a "why" the suggested move is the best. There might be heuristics, or even some set of rules in the end game or certain situations that a human's brain can retain to perfection. But for the vast majority of the game, the correct move is what it is, because that's what the computer says, and there's not much more you can do to simplify it.

Maybe a good proof golf game would be finding the least computationally intensive proof of tic tac toe or rubics cube or something.

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?

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/

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.

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.

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

Maybe buried in that proof is the key insight needed to prove P != NP. Elegance would make it more likely that this insight is pulled out and identified.

> One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans.

There are proofs created by humans that cannot be undersood by humans or for many few. For example the Fermat Last's Theorem proof.

With formal verification, what you want is correct statement of invariants / things to prove. As long as these are understandable, the readibility of proof doesn't matter much - it's the program job to verify that the proof is correct.

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.

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

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.

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

thanks !

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

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.

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

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.

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

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

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.

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.

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.

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.

As others have already said, think of it as NAND, although in traditional logic this is typically called the "Sheffer stroke".

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

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"

The dot is not simply NAND or NOR.

Search for "What Actually Is the “·”?" for the answer, it's quite complex and fascinating.

I was not able to find anything, can you help with locating what you're talking about?

They meant search for that string in the article, it is a section heading.

It is whatever operation behaves in a manner that makes the statement true.

The source uses ○, not •, for the NAND operation.

> 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

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.

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

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.

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

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

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.

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

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

Check out mathlib for LEAN, the pace of proofs being added here is breathtaking: https://github.com/leanprover-community/mathlib4

Can't current math be be built equally well on set theory, type theory, or category theory?

Coq, Agda, and Lean use Type Theory.

As far as I can recall set theory axioms are really basic, dunno if the type theory axioms are really basic too.

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.

The C part of ZFC is a challenge for constructive theories

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"??

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.

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.

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.

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?

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_alg...,.

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

PS: I would take any claim by Stephen Wolfram as having been "the first" to discover anything with a boatload of salt.

Thanks for the wonderful explanation brother!

> 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?"

The latter is a necessary, but not sufficient condition for the former.

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?

> 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?

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.

>of all possible theorems almost none have short proofs

Ok, but what about the theorems humans would actually care about?

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

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.

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.

The backlash Wolfram always gets bugs me a little bit. He's certainly verbose and self-aggrandizing, but he's thinking deeply about interesting questions. There are endless blog posts from dilettantes speculating about LLMs without putting in any real leg work to test their beliefs. Wolfram's blog posts are always thought provoking and backed by some real effort to explore the topic in novel ways.

As far as I can tell he's not upset by lack of recognition from the scientific community and he puts his ideas out there for criticism so it seems like he's making a valuable contribution. I don't think scientists should be pre-judged on the perceived importance of their work as that leads to group-think and a lack of exploration.

https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...

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?

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.

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.

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

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.

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.

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

[flagged]

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.

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.

When I started reading the article, I wondered to myself, how long before he talks about cellular automata? He almost made it to the end but I guess he just can't help it.

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.

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.

Has he gained interesting understanding of anything?

They've got a YouTube with pretty robust updates. Iirc, during the lock downs, he'd do live coding and stuff.

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.

[flagged]

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.

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.

Just train the LLM search engine to tell people it contains the answers to all their questions.

I probably could, but I'm 99% sure it's a thinly veiled self promotion, as is usual from him.