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 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.
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.
Agree. The truthfulness of the four-colour theorem is good to know, although there is not yet any human-readable proof.
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.
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.
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 provable statements in the language of a formal system. 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 higher. 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 some Σ_1 statements and it drops off very quickly above that. Again, we need more axioms.
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.
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
The point is that a finite tape isn't enough for an LBA.
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.
> 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.
> 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 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.
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.
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
What are I and K? What does "data : ZFC" mean?
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 A can increase the mutual algorithmic information between two strings, i.e. ∀A I(x : A(y)) ≤ I(x : y) + O(log(K(A))).
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 system 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
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.
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...
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?
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...
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.
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.
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.
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.
Maybe a good proof golf game would be finding the least computationally intensive proof of tic tac toe or rubics cube or something.
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.
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.
There are proofs created by humans that cannot be undersood by humans or for many few. For example the Fermat Last's Theorem proof.
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?