Hilbert problems

Stream: Formal conjectures

[Seewoo Lee]

Continue from this comment, here are some candidates from Hilbert's problems that might be suitable for the project (modulo significant amount of works):

• 3rd (resolved, Dehn) : Given any two polyhedra of equal volume, is it always possible to cut the first into finitely many polyhedral pieces that can be reassembled to yield the second?
• 5th (partially resolved, Gleason) : Are continuous groups automatically Lie group?
• 7th (resolved, Gelfond-Schneider) : Is $a^b$ transcendental, for algebraic $a \ne 0, 1$ and irrational algebraic $b$ ?
• 8th (partially resolved) :
  • (a) RH
  • (b) For coprime integers $a, b, c$ determine solvability of diophantine equation: $ax + by + c = 0$ for $x$ and $y$ being prime numbers. Goldbach's conjecture and the twin prime conjecture are special cases of this problem.
  • (c) (partially resolved) Generalize results using Riemann zeta function for distribution of prime numbers in integers, to apply them to Dedekind zeta functions for distribution of prime ideals in ring of integers for any number field.
• 10th (resolved, Matiyasevich) : Find an algorithm to determine whether a given polynomial Diophantine equation with integer coefficients has an integer solution.
• 14th (resolved, Nagata) Is the ring of invariants of an algebraic group acting on a polynomial ring always finitely generated?
• 16th (open) : Describe relative positions of ovals originating from a real algebraic curve and as limit cycles on the plane. Also about number of limit cycles of polynomial ODEs.

• 17th (resolved, FC#1678)
  For a polynomial $f \in \mathbb{R}[x_1, \dots, x_n]$, if $f$ takes only nonnegative values, can we express it as a sum of squares of rational functions in $x_1, \dots, x_n$?

• 18th (resolved, Biberbach, Reinhardt, Hales)

  • (a) Are there only finitely many essentially different space groups in n-dimensional Euclidean space?
  • (b) Is there a polyhedron that admits only an anisohedral tiling in three dimensions?
  • (c) What is the densest sphere packing (in $\mathbb{R}^3$)?

The original question was whether it worths to add new directory dedicated to Hilbert's problems, and my current opinion is not to do unless many of above can be actually formalized.
Some of them are easy to add, but not a conjecture anymore (e.g. 3rd or 7th or 17th). For these cases, I think one can check out subsequent works and see if there are any generalizations or variants that are still open.
Some of them already exists in the repository or mathlib or in external projects (e.g. RH). If we really want to make new file for the same problem, we can simply import the existing files for it (I saw this happens for few of Erdos problems).
More importantly, some of them requires significant amount of works. For example, for 14th I couldn't find algebraic group in mathlib yet. But even if we cannot add them at this point, it seems worth to check the problems and see what is missing on mathlib.

[Paul Lezeau]

I think it would be reasonable to add a HilbertProblems subdirectory! (And do the usual imports trick for the cases where this intersects with another subdirectory).

[Paul Lezeau]

And even better if formalising these theorems leads to adding some missing important definitions to Mathlib (that’s one of the goals of formal-conjectures!)

[Seewoo Lee]

Paul Lezeau 말함:

I think it would be reasonable to add a HilbertProblems subdirectory! (And do the usual imports trick for the cases where this intersects with another subdirectory).

I made new directory FormalConjectures/HilbertProblems in FC#1678.

[Joseph Myers]

The formal-conjectures README mentions "solved statements from dedicated problem lists" as in scope, but I don't know if there needs to be some kind of date cut-off. https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_mathematics has a section "Problems solved since 1995" so an implicit cut-off for what goes on that page at all. On the whole I think Hilbert's problems are mathematically interesting enough to be worth formally stating (including different variants on how people have interpreted the problems over time, results people have proved relating to them that might not be strictly part of Hilbert's original statements, etc.) - and indeed worth formalizing proofs of - even though some were solved a long time ago.

[Joseph Myers]

Commenting specifically on Hilbert's 18th problem, part 3: although it's commonly considered to be the Kepler conjecture, Hilbert asked more generally about "equal solids of given form, e.g., spheres with
given radii or regular tetrahedra with given edges". The fully general form (copies of a completely arbitrary solid) is probably too general and vague to admit a meaningful formal description of what a solution (the function from a solid to the maximum density of a packing?) would be. But the explicitly mentioned case of regular tetrahedra is very far from being solved (the answer is known to be somewhere between $\frac{4000}{4671}$ and $1 - 2.6\times10^{-25}$). So you could definitely give a formal statement of that as an open problem and count it as part of a Hilbert problem.

[Joseph Myers]

As for Hilbert's 18th problem, part 2, I need to get several more PRs from AperiodicMonotilesLean (which includes definitions of isohedral number of tilings and protosets in a discrete context) into mathlib, then develop corresponding material in a continuous context and get that into mathlib as well, in order to have the concept of "anisohedral". And then we also need a definition of a polyhedron in mathlib as well (in this context, where a polyhedron is interpreted as a solid body, not necessarily convex, not necessarily simply connected either, but probably bounded and with connected interior - although there are in fact convex polyhedra that answer the question, Reinhardt didn't come up with such examples).

[Seewoo Lee]

Thank you for all the information - I didn't realize that. This seems to be the paper you mentioned for the lower bound of tetrahedral packing.

[Joseph Myers]

And https://arxiv.org/abs/1008.2830 has the upper bound. (The fact that you can't make a solid angle of $4\pi$ from the angles at the vertices and edges of a regular tetrahedron implies they don't tile space, and it's fairly clear that you could in principle turn that into an upper bound strictly less than 1 on the density of a packing, which is what they did.)