Challenging proofs

Stream: general

[Martin Dvořák]

Please, give me some examples of really challenging formal proofs (not necessarily in Lean). I am not looking for something that took 50k lines of code to prove. I'd rather have some examples of proofs that look trivial on paper but take, let's say, 500 lines to prove formally.

[Yaël Dillies]

Sperner's lemma

[Yaël Dillies]

The paper proof takes two pages and is easy combinatorics. It actually glosses over the most difficult part of the proof: Showing that every edge in a triangulation belongs to exactly two triangles if it's inside or one triangle if it's on the boundary.

[Yaël Dillies]

We need a fair chunk of branch#sperner-again (6k lines!) to prove that statement (and we actually haven't proved it yet).

[Yaël Dillies]

Szemerédi's regularity lemma

Again, two pages on paper. Took us roughly all of branch#szemeredi. Particularly handwavy was the construction of the new partition during the induction. It's fairly hard to prove that it's a partition and even harder to show that it is equitable.

[Martin Dvořák]

Thank you! But can you point me to something more trivial on paper?

[Yaël Dillies]

I'm sure Kevin can jump in and tell us about his ZFC vs type theory issues.

[Chris Birkbeck]

How long is the snake lemma in lean? I bet that takes a lot more lines than it does on paper.

[Riccardo Brasca]

It's long, but to be honest I've seen a proof that works in any abelian category

[Riccardo Brasca]

Without using Freyd-Mitchell

[Andrew Yang]

It's about 1200 lines in LTE. With another 400 or so providing a pseudoelement API.

[Riccardo Brasca]

Personally I find working with expression like (-1) ^ (n * (n - 1) / 2), where n : ℕ extremely annoying, because of nat division

[Riccardo Brasca]

(I am not suggesting we should change it, it is just annoying, that's life)

[Oliver Nash]

The interior of a triangle (in the Euclidean plane) is the set of points with strictly positive barycentric coordinates.

[Yaël Dillies]

Oh yes, thanks for doing that, Oliver. I'm actually pretty sure it will come up in Sperner's lemma.

[Oliver Nash]

Ha, that would be great!

[Martin Dvořák]

On the side of really trivial proofs, is this a 40-line-long proof that subgroups of cyclic groups are cyclic?

https://github.com/leanprover-community/mathlib/blob/ee36571eafb8d603b18fb5db1313bb71ded3a29c/src/group_theory/specific_groups/cyclic.lean#L163

[Wenda Li]

Here are some examples: https://lawrencecpaulson.github.io/2022/01/12/Proving-the-obvious.html. When formalising Modular Functions and Dirichlet Series in Number Theory by Tom M. Apostol, some one-line proofs can take hundred lines of proofs.

[Martin Dvořák]

Martin Dvořák said:

On the side of really trivial proofs, is this a 40-line-long proof that subgroups of cyclic groups are cyclic?

https://github.com/leanprover-community/mathlib/blob/ee36571eafb8d603b18fb5db1313bb71ded3a29c/src/group_theory/specific_groups/cyclic.lean#L163

Oh wait. It isn't only about finite cyclic groups, right? Then the length isn't surprising to me anymore.

[Yakov Pechersky]

docs#parser.nat_eq_done, 2 thousand lines to say that parsing in digits gives you a number

[Patrick Johnson]

See also the Poincare-Bendixson Theorem. It is trivial to prove on paper, but it took several months and more than 7K lines of code to formalize it. The proof is formalized by Fabian Immler and Yong Kiam Tan in Isabelle/HOL.

[Vincent Beffara]

Well the wiki page you are linking says "A weaker version of the theorem was originally conceived by Henri Poincaré (1892), although he lacked a complete proof" so that would kind of put a high bar on triviality to count this one as an example :upside_down:

[Yakov Pechersky]

Regarding the 2k lines, most of that 2k is building a general and powerful api for any parser built on top of the combinators that core lean provides.

[Yakov Pechersky]

It just happens to be the case that the nat parser (docs#parser.nat) uses several of those combinators

[Vincent Beffara]

And the 6k lines about Sperner seem to also contain a big chunk on simplicial complexes

[Yaël Dillies]

My point is that you aren't expecting to need to talk about simplicial complexes at all!

[Patrick Johnson]

Well the wiki page you are linking says "A weaker version of the theorem was originally conceived by Henri Poincaré (1892), although he lacked a complete proof" so that would kind of put a high bar on triviality to count this one as an example

My understanding is that Poincaré had been missing some math tools that were invented later. The main part of the theorem (modulo some technical details that are easy to formalize anyway) can simply be proved by drawing a sketch. However, formalizing that sketch is far from trivial.

[Vincent Beffara]

Well, it would be this or embedding into the plane with edges sent to continuous paths and then you need to prove the Jordan curve theorem or something (is that in mathlib BTW?), or you first restrict to triangulations that can be realized using straight edges but that's another can of worms ... in that particular case I don't find 6k lines to be overblown

[Yaël Dillies]

Pretty sure we don't have JCT

[Kevin Buzzard]

Cubing the cube took Floris 300+ lines and the argument can be passed between mathematicians pretty easily.

[Kevin Buzzard]

The proof that if you tile a regular hexagon with lozenges then an equal number point in each direction is one picture but that would be tricky to formalise

[Yaël Dillies]

I think tilings in general are hard to formalize. I'm wondering whether we should define discrete tilings from continuous ones. And I don't know where Wang tiles fit.

[Kevin Buzzard]

They fit on my bathroom wall

[Heather Macbeth]

I have loose plans for an undergrad project on this, from the point of view of "discrete subgroups of the affine isometry group of the plane".

[Yaël Dillies]

That's what I was thinking too, but I wondered whether I was missing the greater picture.

[Yaël Dillies]

Btw, subgroups are probably too restrictive to talk about aperiodic tilings and multitilings, like Penrose's.

[Yaël Dillies]

The most general definition I could come up with is

-- `ι` is the type of tiles, `α` is the space
structure tiling (ι 𝕜 α : Type*) [many_typeclasses_on α] :=
(tiles : ι → set α)
(copies :  ι → set (α →ᵃⁱ[𝕜] α))
(union (a : α) : ∃ i (f ∈ copies i), a ∈ copies i '' tiles i)
-- equivalently, `⋃ i, (copies i).seq (tiles i) = univ`
(disjoint : (⋃ i, (λ f : α →ᵃⁱ[𝕜] α, f '' tiles i) '' copies i).pairwise_disjoint id)

[Yaël Dillies]

Potentially, you want to pull tiles out of the structure and generalize away from set α

[Yaël Dillies]

Namely,

-- `ι` is the type of usable tiles
-- `α` is the type of possible tiles
-- `F` is the type of transformations
structure tiling (ι 𝕜 F α : Type*) [complete_lattice α] [fun_like F α (λ _, α)] :=
(tiles : ι → α)
(copies :  ι → set F)
(union : ⨆ i (f ∈ copies i), (f : α → α) (tiles i) = ⊤)
(disjoint : set.univ.pairwise_disjoint copies)

[Yaël Dillies]

@Anne Baanen, can we turn docs#set.image into the instance

instance [fun_like F α (λ _, β)] : fun_like F (set α) (λ _, set β)

or is it dangerous?

[Alex J. Best]

This is quite close to docs#measure_theory.is_fundamental_domain of course, maybe you can take some inspiration from there. In particular it seems like disjoint is too strong a condition if you want the tiles to be closed sets then they won't be disjoint (only almost everywhere disjoint), but if you want them to be open they won't cover

[Yaël Dillies]

I think the above definition is very general. It works for tilings of the plane (by setting α := set α, F := affine isometries or orientation-preserving affine isometries) or maybe not because topology, finite tilings (by setting α := finset α or a custom tile type, eg. finset (fin m) × finset (fin n) for dominos in the $m \times n$ board, F := custom transformations).

[Vincent Beffara]

Alex J. Best said:

This is quite close to docs#measure_theory.is_fundamental_domain of course, maybe you can take some inspiration from there. In particular it seems like disjoint is too strong a condition if you want the tiles to be closed sets then they won't be disjoint (only almost everywhere disjoint), but if you want them to be open they won't cover

But what if my preferred tiles have a boundary with positive measure? :-)

[Yaël Dillies]

I swear we aren't out of the woods!

[Alex J. Best]

I guess you can also make the definition using only topological properties. This is something that has always confused me, for a fundamental domain as in the above definition is the topological boundary always the same as the intersection with the translates if we start with a closed set?

[Yaël Dillies]

That rules out using the same definition for continuous and discrete tilings, because there's no way we will use this stuff topology on finset, right?

[Anne Baanen]

Yaël Dillies said:

Anne Baanen, can we turn docs#set.image into the instance

instance [fun_like F α (λ _, β)] : fun_like F (set α) (λ _, set β)

or is it dangerous?

What do you want to happen if f is something polymorphic and α = set α'? Should f be applied to the set or pointwise to each element of the set? (Typeclass-technically it's also problematic since α and β are out_params, so for fixed F should only take one value.)

[Yaël Dillies]

Yeah unfortunately I think that's not really doable.

[Yaël Dillies]

So that prevents us from generalizing away from set/finset unless we use functor trickery.

[Joseph Myers]

If you want to define tilings formally, I think it might make sense to start from some existing informal definitions, such as that of Grünbaum and Shephard in Tilings and Patterns tandp1.png and that of Goodman-Strauss, and consider what aspects of the definition are essential and what should be generalized.

I think the "closed" part of the definition - the involvement of topology, with only interiors required to be disjoint - is essential. While people do consider tiling problems where a tile includes some boundary points but not others and every point (of the plane, 3-space, etc.) must be covered exactly once, they feel very different from most tiling problems where points on boundaries are expected to be covered more than once (and in any case, they are just a special case of the topological version, when you take the discrete topology). If you don't want to involve topology for working formally with discrete tilings, that probably indicates having appropriate separate definitions such as discrete_tiling, and explicit equivs and lemmas translating between those definitions and the general topological ones in the case of the discrete topology.

On the other hand, restricting to the plane, or a "non-compact metric $n$-manifold" as Goodman-Strauss does, is unnecessary and would prevent the definition from covering discrete tilings. The "countable" constraint in Grünbaum and Shephard is unnecessary (that's simply a particular choice of index type, and the index type would be a parameter to definitions such as tiling). "compact" and "closure of its interior" for tiles, as suggested by Goodman-Strauss, don't seem to be needed for a general definition; they're simply conditions for being well-behaved that could be hypotheses on relevant theorems, much like "tiles are closed topological discs" or "the tiling is locally finite". Likewise any constraint that a protoset of tiles is finite; again, that's just another choice of index type.

I think key insights in Goodman-Strauss's definition include (a) that the space being tiled comes with some group of automorphisms and (b) defining a tiling of a given protoset of tiles is more interesting than defining a tiling in isolation from a choice of protoset.

So I'd be inclined to start by defining a tiling_space to be a topological space together with a subgroup G of the group of homeomorphisms of that space (typically it would be a metric space and a subgroup of isometries, quite likely all isometries or all orientation-preserving isometries, but I don't think that needs to go in the most general definition; in the discrete case this would become a group of permutations). A tiling space is a context in which you can both define tilings by a protoset of tiles and have concepts (looser than equality) of whether two tilings are the same.

Then we need to define a protoset of tiles in a tiling_space. That would be an indexed family. For each index value, there would be both the tile itself (a closed set) and a subgroup of its stabilizer under the obvious action of G. The point of specifying that subgroup is to cover the common case where tiles are considered to be marked in order to reduce their symmetries; an unmarked tile corresponds to taking the whole of its stabilizer.

Then to define a tiling (or packing, or covering - an indexed family of tiles from a protoset, which may be required to satisfy certain other conditions), given a tiling space, a protoset and an index type for the tiling itself, for each value of that index type you specify (a) a value of the index type for the protoset and (b) an element of G, that maps that tile from the protoset to its position in the tiling.

This doesn't do anything special to handle matching rules - those would need to be some extra predicate applied to a tiling to decide whether it's valid or not.

Given the above, there are two natural notions of whether two tiling objects are the same. One - same tiles in same positions and orientations - is that they are equivalent under an equiv of the index types of the tilings, together with multiplying each specified element of G on the right by some element of the specified subgroup of the stabilizer for that tile. Another is that they are equivalent if they are related by the above together with transforming the whole tiling by the same element of G.

Note that I suspect there are no mathematically interesting results to be proved about tiling in such generality - to get anything interesting, you need to start imposing extra constraints on the tiling space, tiles and tiling. And results on tiling in the literature don't generally come with any thought on what the most general context in which they might hold is - they're more likely just to be stated for e.g. locally finite plane tilings by closed topological discs, if the authors even state such precise conditions at all.

[Yaël Dillies]

I was mostly interested in a definition of finite tilings, and was hoping that we could use the same definition for both finite and infinite tilings.

[Joseph Myers]

Heather Macbeth said:

I have loose plans for an undergrad project on this, from the point of view of "discrete subgroups of the affine isometry group of the plane".

I wonder how accessible Bieberbach's theorems on space groups are for formalization.

[Joseph Myers]

Kevin Buzzard said:

Cubing the cube took Floris 300+ lines and the argument can be passed between mathematicians pretty easily.

The proof in the mathlib archive assumes (as part of the formal problem statement) that all the cubes have the same orientation as the one being cubed. It wouldn't surprise me if it's substantially harder to formalize a proof that, if you tile a cube with finitely many cubes, they do all have the same orientation (which is even more obvious to humans).

[Patrick Massot]

I would count that as a failure of human intuition assessing difficulty. In the same way the Kepler conjecture is "obvious".

[Daniel Roca González]

@Yaël Dillies When you say finite tiling/discrete tiling/continuous tiling what do you mean?

[Yaël Dillies]

Like, domino tilings, the mutilated checkerboard problem...

[Yaël Dillies]

I have a dozen of such problems that would be fun to formalize for imoists.

[Daniel Roca González]

I mean, what do the properties "discrete", "finite", "continuous" for tilings mean? I don't think these terms are well established... (Although when it comes to tilings there is not much agreement on how to define things unfortunately).

[Daniel Roca González]

Is it about the shape of the tiles? The space that is being covered?

[Yaël Dillies]

The space that is being covered

[Yaël Dillies]

Discrete vs continuous tiling is a matter of the space itself being discrete or continuous. Finite is about the space being finite.

[Daniel Roca González]

I'm pretty sure the definition for topological spaces should technically cover all cases. A tiling of a topological space is a set of tiles that covers the whole space, such that the tiles intersect only at their boundaries. If the space is Z^2 we can make the tiles be finite sets of points and the condition is trivial.

[Daniel Roca González]

The question is how cumbersome that gets...

[Yaël Dillies]

Yes sure, but you see how no finite combinatorialist will want to bother about the topology?

[Daniel Roca González]

Yes, of course.

[Julian Berman]

Tangential to the original question, /r/math seems to be discussing long proofs that are now short today. Maybe some day this will be an interesting question to ask about specific proofs in mathlib's git history :)

[Eric Wieser]

I look forward to us claiming the "shortest" proof of FLT (measured by lines in git), lemma flt : _ := flt_old