Zulip Chat Archive

Stream: maths

Topic: some newbie questions about following progress


Mario Krenn (Jun 22 2021 at 14:14):

Pls let me ask another newbie question. I read that proofs are usually done outside of mathlib, and only afterwards imported. Also, only if code is imported in mathlib, it is save for future updates. How about proofs huge proofs like those from the LTE or the definitions in the perfectoid spaces, are they in mathlib? Other, more elementary proofs like the Hall's marriage problem (asking as i saw the paper and talk about it by @Alena Gusakov), is that in mathlib or only available externally?

Is there some place where i can see all defintions/theorems that are included, and progress (i.e. when new theorems are included)? I am sure this infos is available in the docs, but there is so much data for beginners, i failed atm to understand these super basic questions. Thanks :)

Johan Commelin (Jun 22 2021 at 14:22):

@Mario Krenn we make an effort to move as much as possible into mathlib. For now, LTE contains a directory called for_mathlib. It used to have > 7000 lines of code, but in the past 2 weeks, we've got it down to 5500 lines. My hope is that around the summer break we'll have cut that number in half.

Johan Commelin (Jun 22 2021 at 14:23):

https://leanprover-community.github.io/mathlib-overview.html and https://leanprover-community.github.io/undergrad.html might answer some of your questions as well

Eric Rodriguez (Jun 22 2021 at 14:24):

Alena's work on hall is in here, which is part of Mathlib

Yaël Dillies (Jun 22 2021 at 14:24):

Our current approach is to keep the big specialized projects outside of mathlib (see here)), and some of it (IMO problems, the sensitivity conjecture) is also in the directory archive/

Eric Rodriguez (Jun 22 2021 at 14:25):

awh, I didn't know we did the sensitivity conjecture; that proof is so great

Yaël Dillies (Jun 22 2021 at 14:26):

It is! And even the Lean proof isn't that long.

Alena Gusakov (Jun 22 2021 at 14:48):

aw i wanted to do that one lmao

Yaël Dillies (Jun 22 2021 at 15:02):

Don't be sad! That means mathlib is moving fast.

Mario Krenn (Jun 22 2021 at 15:15):

Thanks for the answers, that gives me some very interesting directions.

Patrick Massot (Jun 22 2021 at 15:57):

We did the sensitivity conjecture proof one year and a half ago, a couple of months after it appeared on paper.

Kyle Miller (Jun 22 2021 at 16:07):

Mario Krenn said:

Is there some place where i can see [...] progress

One answer to this is the PR list on github: https://github.com/leanprover-community/mathlib/pulls

For example, this is where the proof of Hall's theorem lived for a couple months as it got polished for inclusion. (It's even still somewhat in development, with a PR to give the non-finite version.)

Mario Krenn (Jun 22 2021 at 16:16):

This is slightly related to following progress. How would i see what happens to Hall's marriage Theorem? I see this page (https://leanprover-community.github.io/mathlib_docs/combinatorics/hall.html), but does it say something about when the individual generalizations have been added? Also, i am curious how complex it is to generalize further to non-bipartite graphs, i.e. Tutte's Theorem? (i am talking about the HMT because this is the entry point that interests me most, and is probably closest related to my own work in an entirely different field of quantum physics)

Bryan Gin-ge Chen (Jun 22 2021 at 16:19):

If you click on the "source" link on the right, you'll be directed to this GitHub page which lets you browse the history of the file / git blame, etc. Does that help?

Kyle Miller (Jun 22 2021 at 17:19):

I think it might be easiest to prove Tutte's theorem from scratch because, unlike Hall's theorem, it seems to make use of graphs in an essential way. Once @Yaël Dillies PR's the formalization of walks and connected components for simple graphs, then it will be a bit easier to state the theorem, but even so it's not so bad:

import data.finset
import data.fintype.basic
import combinatorics.simple_graph.basic
import combinatorics.simple_graph.matching

open_locale classical
noncomputable theory
open function fintype

variables {V : Type*} [fintype V]

/-- Restricting to a subset `W`, give vertices in the connected component of a vertex -/
def simple_graph.component (G : simple_graph V) (W : finset V) (v : W) : finset V :=
W.filter (λ w, quot.mk G.adj w = quot.mk G.adj v)

/-- Restricting to a subset `W`, give the connected components. -/
def simple_graph.components (G : simple_graph V) (W : finset V) : finset (finset V) :=
W.attach.image (G.component W)

theorem tutte
  (G : simple_graph V) :
  ( (M : G.matching), M.is_perfect)
     ( (W : finset V),
       ((G.components W).filter (λ (C : finset V), odd C.card)).card  card V - W.card) :=
sorry

Yaël Dillies (Jun 22 2021 at 17:48):

Eh, it may be my PR, but it's your code :smile:


Last updated: Dec 20 2023 at 11:08 UTC