Optimization constants

Stream: Formal conjectures

[Felix Pernegger]

There is a new project / GitHub repository about the optimizations of constants in open problem (i.e. exponent of matrix multiplication complexity), see the announcement here. (EDIT: Note this is not a Lean repository, but rather aims to serve as an overview.)
Per discussion at this, it may be nice to add Lean formalisations to definitions (and bounds etc) of constants defined there, similar as it is being done for Erdos problems. Note the numbering system of the constants is still not stabilized. Most of the constants are likely also more difficult to formalise than Erdos problems.
The formal conjectures repository would probably be suitable for this endeavor.

I was thinking each constant should have the definition, formalisation of best known lower and upper bounds, answer(sorry) for a lower and upper bound as well as conjectures about the constants if they exist.

Would this make sense to add (as its own folder)?

[Yaël Dillies]

I am somewhat confused as to what the difference with formal-conjectures is. A lot of our problems are about optimising constants too

[Felix Pernegger]

I mainly meant if this could become its own folder (like Green open problems and Erdos problems), since that would make it easier to link to.

[Yaël Dillies]

Oh I see, Terry's repo isn't specifically about Lean. Sure, that could be an idea!

[Yaël Dillies]

Felix Pernegger said:

Most of the constants are likely also more difficult to formalise than Erdos problems

Although this hasn't yet resulted in a change of policy, consensus is building up at GDM that the current contributions to formal-conjectures are often too elementary in nature, and that we would instead like to see some harder stuff. So these constants being difficult to formalise is a good thing!

[Felix Pernegger]

Yaël Dillies said:

Felix Pernegger said:

Most of the constants are likely also more difficult to formalise than Erdos problems

Although this hasn't yet resulted in a change of policy, consensus is building up at GDM that the current contributions to formal-conjectures are often too elementary in nature, and that we would instead like to see some harder stuff. So these constants being difficult to formalise is a good thing!

Yes, I can imagine having 10 differents versions of "Are there infinitely many prime of the form xyz?" isnt terribly useful :)

[Paul Lezeau]

Felix Pernegger said:

Yes, I can imagine having 10 differents versions of "Are there infinitely many prime of the form xyz?" isnt terribly useful :)

To be clear, I think adding such conjectures isn’t an issue per say, but rather that these form only a subset of the problems that mathematicians are interested in so it would be nice for formal-conjectures to reflect that!

[Joseph Myers]

Yaël Dillies said:

Felix Pernegger said:

Most of the constants are likely also more difficult to formalise than Erdos problems

Although this hasn't yet resulted in a change of policy, consensus is building up at GDM that the current contributions to formal-conjectures are often too elementary in nature, and that we would instead like to see some harder stuff. So these constants being difficult to formalise is a good thing!

The harder something is to state, the more important it is to get all the underlying definitions and API for them into mathlib first to improve confidence that the formal statement is actually talking about the correct objects, rather than accumulating lots of non-elementary definitions in formal-conjectures where they probably haven't had much review from relevant experts.

I'm sure someone must have written a taxonomy of different ways in which mathematics can be hard, if not one specifically in the context of formalization. You can have things that are hard to formalize because of long chains of missing definitions but where those definitions are themselves quite elementary; you can also have cases where the definitions are not at all elementary, or where writing down good definitions (or proving those definitions make sense) itself depends on proving lots of theorems. You can also have cases where the problem isn't writing down some formal definitions that work for a specific conjecture, but producing good and general definitions that are reasonable to work with in a formal context. And then you can have things that are very hard and non-elementary to prove but easy and elementary to state (like FLT) - but when formalizing a conjecture, you don't know what would be involved in a solution.

[Joseph Myers]

And then there are lots of interesting open problems of the form "classify X" or "understand Y" that inherently don't admit a formal statement until you have a better idea of what the answer is likely to look like, but those seem like they are inherently outside the scope of formal-conjectures.

[Moritz Firsching]

Good points, identifying missing defintions that allow to formulate lots of conjectures and upstreaming those relevant definitions is of course one goal of formal-conjectures!

[Yaël Dillies]

Joseph, you are preaching to the choir :wink:

[Moritz Firsching]

There is at least some support for more open ended questions, using the answer(sorry) mechanism to allow gaps of certain type. This makes it in principle at least possible to formalise "classify all X" in some cases. Of course provided a solution one has to decide if it was really a solution. I agree that there are open problems that doesn't map to anything formal, like Hilberts 23rd problem: Further development of the calculus of variations

[Terence Tao]

Hi, just to say that I would be very happy to have a linkup between the optimization constants repository and the formal conjectures repository, similar to the linkages with the Erdos problem repository.

I think we've now settled on a stable numbering system: every constant will be labeled Nx, where N is a natural number indicating the family of constants it belongs to, and x is a letter of the alphabet, defaulting to a (so Na can be abbreviated as N, though the file containing the constant will be named Na.md rather than N.md for forward compatibility). Hopefully, once a constant is assigned an Nx label, it will stay that way forever, barring some exceptional situation with duplicates or something.

For an immediate formalization challenge, I'd be interested to see whether $C_{14}$ (the smallest $n$ for which $BB(n)$ is undecidable) can be formalized within Lean.

[Moritz Firsching]

Great idea, I really like the project and have some favorite constants that I plan to add!

For some of the problems we already have a formalisation, for instance https://github.com/google-deepmind/formal-conjectures/blob/169aaebeb73230c97bcf87e2a3b73ed2b202de46/FormalConjectures/ErdosProblems/36.lean#L181-L209.

For some of the constants, I suppose there could be different levels of rigor proving stuff about constants:

• "normal" computations, like floating points with the usual caveats
• more rigorous computation, like interval arithmetic, SAT solvers, optimise LPs over rational numbers..
• Lean proofs (or in some other system), using native_decide or not.
  Of course formal-conjectures is likely only to capture the last of those. Although perhaps we could make our categorization for "research solved" more fine-grained here.

[Moritz Firsching]

Terence Tao said:

For an immediate formalization challenge, I'd be interested to see whether $C_{14}$ (the smallest $n$ for which $BB(n)$ is undecidable) can be formalized within Lean.

we already have some stuff on BusyBeavers: https://github.com/google-deepmind/formal-conjectures/blob/169aaebeb73230c97bcf87e2a3b73ed2b202de46/FormalConjecturesForMathlib/Computability/TuringMachine/BusyBeavers.lean, perhaps this makes a good start for this!

[Bolton Bailey]

Moritz Firsching said:

perhaps this makes a good start for this

Also helpful is the fact that the second incompleteness theorem has been formalized in Lean (thread: #maths > Gödel's Incompleteness Theorem @ 💬 )

This seems tricky though. As I understand it, the task we would need to undertake to prove that "there is an n for which BB(n) is undecidable in ZFC" would not be just to define the Turing Machines and the Busy Beaver function in Lean, but to define these concepts within a model of ZFC within Lean.