Who Can Understand the Proof? A Window on Formalized Mathematics

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.

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.

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

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.

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

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.

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

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.

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

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

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

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

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

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.

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

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.

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.

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.

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

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

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.