some newbie questions about following progress

Stream: maths

[Mario Krenn]

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]

@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]

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]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

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

[Alena Gusakov]

aw i wanted to do that one lmao

[Yaël Dillies]

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

[Mario Krenn]

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

[Patrick Massot]

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

[Kyle Miller]

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]

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]

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]

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]

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