## Stream: general

### Topic: Challenging proofs

#### Martin Dvořák (Jan 24 2022 at 12:48):

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.

Sperner's lemma

#### Yaël Dillies (Jan 24 2022 at 12:50):

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 (Jan 24 2022 at 12:52):

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 (Jan 24 2022 at 12:56):

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 (Jan 24 2022 at 12:56):

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

#### Yaël Dillies (Jan 24 2022 at 12:57):

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

#### Chris Birkbeck (Jan 24 2022 at 13:04):

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

#### Riccardo Brasca (Jan 24 2022 at 13:05):

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

#### Riccardo Brasca (Jan 24 2022 at 13:06):

Without using Freyd-Mitchell

#### Andrew Yang (Jan 24 2022 at 13:06):

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

#### Riccardo Brasca (Jan 24 2022 at 13:10):

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

#### Riccardo Brasca (Jan 24 2022 at 13:10):

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

#### Oliver Nash (Jan 24 2022 at 13:14):

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

#### Yaël Dillies (Jan 24 2022 at 13:16):

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

#### Oliver Nash (Jan 24 2022 at 13:16):

Ha, that would be great!

#### Martin Dvořák (Jan 24 2022 at 13:17):

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 (Jan 24 2022 at 13:19):

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 (Jan 24 2022 at 13:36):

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 (Jan 24 2022 at 13:40):

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

#### Patrick Johnson (Jan 24 2022 at 13:40):

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 (Jan 24 2022 at 13:43):

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 (Jan 24 2022 at 13:44):

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 (Jan 24 2022 at 13:45):

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

#### Vincent Beffara (Jan 24 2022 at 13:46):

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

#### Yaël Dillies (Jan 24 2022 at 13:48):

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

#### Patrick Johnson (Jan 24 2022 at 13:55):

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 (Jan 24 2022 at 13:55):

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 (Jan 24 2022 at 13:56):

Pretty sure we don't have JCT

#### Kevin Buzzard (Jan 24 2022 at 14:53):

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

#### Kevin Buzzard (Jan 24 2022 at 14:54):

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 (Jan 24 2022 at 14:57):

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 (Jan 24 2022 at 14:58):

They fit on my bathroom wall

#### Heather Macbeth (Jan 24 2022 at 14:59):

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 (Jan 24 2022 at 15:00):

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

#### Yaël Dillies (Jan 24 2022 at 15:01):

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

#### Yaël Dillies (Jan 24 2022 at 15:16):

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 (Jan 24 2022 at 15:24):

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

#### Yaël Dillies (Jan 24 2022 at 15:35):

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 (Jan 24 2022 at 15:36):

@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 (Jan 24 2022 at 15:40):

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 (Jan 24 2022 at 15:42):

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 (Jan 24 2022 at 15:45):

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 (Jan 24 2022 at 15:49):

I swear we aren't out of the woods!

#### Alex J. Best (Jan 24 2022 at 15:52):

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 (Jan 24 2022 at 15:53):

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 (Jan 24 2022 at 16:07):

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 (Jan 24 2022 at 16:23):

Yeah unfortunately I think that's not really doable.

#### Yaël Dillies (Jan 24 2022 at 16:24):

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

#### Joseph Myers (Jan 24 2022 at 20:44):

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 (Jan 24 2022 at 20:46):

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 (Jan 24 2022 at 20:48):

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 (Jan 24 2022 at 20:52):

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 (Jan 24 2022 at 20:53):

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 (Jan 24 2022 at 21:00):

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

#### Yaël Dillies (Jan 24 2022 at 21:00):

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

#### Yaël Dillies (Jan 24 2022 at 21:01):

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

#### Daniel Roca González (Jan 24 2022 at 21:02):

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 (Jan 24 2022 at 21:03):

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

#### Yaël Dillies (Jan 24 2022 at 21:04):

The space that is being covered

#### Yaël Dillies (Jan 24 2022 at 21:05):

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 (Jan 24 2022 at 21:07):

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 (Jan 24 2022 at 21:08):

The question is how cumbersome that gets...

#### Yaël Dillies (Jan 24 2022 at 21:09):

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

Yes, of course.

#### Julian Berman (Jan 24 2022 at 22:59):

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 (Feb 24 2022 at 08:47):

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

Last updated: Aug 03 2023 at 10:10 UTC