Navier-Stokes Announcement

Yes, you can make problems arbitrarily complex. But the prize problems were chosen not just because the solutions appear likely to be very complex (the problem statements aren't necessarily inherently complex--there is a way to restate the Riemann hypothesis that a junior high school student could easily understand, which I'll give below).

They were chosen because they were important problems that mathematicians really wanted solved, top people had worked on them for a long time and progress stalled a long time ago, and it seemed likely that solving them would require major breakthroughs.

Those kind of problems can be discouraging. Enough people who are probably better than you have spent enough time failing to solve them that realistically most researchers are going to focus all their efforts on something they are likely to make progress on.

A nice prize can get more people to at least work on them as side projects.

Here's that restatement of the Riemann hypothesis I mentioned.

The Riemann hypothesis is that the non-trivial zeros of the function ζ(s) occur on the line 1/2 + yi.

ζ(s) is 1/1^s + 1/2^2 + 1/3^s + ... when s is a complex number whose real part is greater than 1, and defined everywhere else except s = 1 by a process called analytic continuation. The trivial zeros are at s = -2, -4, -6, ... .

For a mathematician, or a non-mathematician who has taken complex analysis and hasn't forgotten much of that, that is not too complex a definition. For anyone else the first reaction is probably "Trivial zeros? How the heck does that thing even have zeros? And if it does how the heck can it have zeros at any negative integers! It is obviously infinity at every negative integer!!!".

Here's a different hypothesis that turns out to be exactly equivalent to the Riemann hypothesis. They are either both true of both false, so resolving one of them resolves the other.

Let H(n) = 1 + 1/2 + ... + 1/n for all positive integers n. These are called the harmonic numbers.

Let S(n) = the sum of the positive integer factors of n for all positive integers n. For example S(4) = 1 + 2 + 4, S(6) = 1 + 2 + 3 + 6, and S(17) = 1 + 17.

Hypothesis: S(n) The proof that this is equivalent to the Riemann hypothesis is here [1].

[1] https://arxiv.org/pdf/math/0008177

Semantic versioning describes the following idealized setup:

- you have an interface you expose (a contract, and thus a contract signature)

- you do not change the contract signature -> patch version bump

- you do change it but in a non-breaking way (e.g. additively) -> minor version bump

- you do change it but in a breaking way (e.g. mutatively or destructively) -> major version bump

One would expect then that since interface signatures are statically derivable, semantic version tags can be auto-assigned. And indeed, in lots of shops that's exactly what happens (in my opinion, correctly).

The problem with this is that it comes with a lot more smoke than fire. The interface having no changes or non-breaking changes doesn't mean the actual code behind those interfaces is not going to cause a breakage. It literally is just about the interface itself.

And so unless you encode absolutely everything about the semantics your implementation actually observes into the interface, which is what the semver specification asks you to do so as their sleight of hand, this means the interface will be a leaky abstraction. Which means that external software interfacing with yours may observe behavior that is beyond the purview of semantic versioning. Which means that they do. Which means that they absolutely can and will break, and your package managers' fancy version constraint syntax exists to make such fun events happen.

The way this is usually handled then is:

- you live with the pain: acknowledge the limitations of semver, accept you've been duped, and just give in

- you have human release managers assign versions manually, based on whole program and whole system semantics (with the human overhead and error that entails), falsely claiming that what you're doing is still semver

- you switch to a less deceptive versioning scheme, like calendar versioning; as a bonus, you now no longer have to pretend that your entire application somehow only has a single unified interface

This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface. The way the proof is derived may expose semantic gaps in the statement itself, and (ab)use them to obtain the logical consistency certificate. Hence, a vacuous proof, and hence why this is not statically assertable to be not the case. It is part of the challenge in asserting that the statement was correctly formalized in the first place: you need to manually identify whether the way the consistency was achieved is actually meaningful, or just a formalization gap.

Which really makes me wonder about the actual value proposition of Lean then, but alas...

Can only be false if there is an instance where A is true, and B is false. In all other cases it's true, even when A is always false.

That's the key.