Brooks' theorem

Stream: Is there code for X?

[Shuhao Song]

It was mentioned in this thread #narrow/stream/113489-new-members/topic/Graph.20theory.20project, but I'm not sure if it has been formalized yet.

[Yaël Dillies]

Oh someone at my workshop in Aalto yesterday is wanting to formalise it. It's definitely not formalised yet.

[Shuhao Song]

And how about the Bondy–Chvátal theorem about Hamiltonian path? If it was not formalized yet, I would like to start the project.

[Yaël Dillies]

Never heard anyone claiming to work on it, but you never know :shrug:

[Shuhao Song]

After 3 days of work it finished, and it contains Dirac's theorem and Ore's theorem as corollary. https://github.com/meow-sister/mathlib4

[Shuhao Song]

Note that the code is really messy. I'd like to do some cleanup later.

[Shuhao Song]

The formalization of Ore's theorem was not correct initially, and it was fixed now.

[Yaël Dillies]

Please PR!

[Shuhao Song]

Yaël Dillies said:

Please PR!

How can I "ask for write permission to a non-master branch" according to https://leanprover-community.github.io/contribute/index.html?

[Shuhao Song]

Note that the code needs cleaning up. It contains many parts: some theorems about List, some theorems about Walk, the definition and properties of the fixed point of function $f : X \rightarrow Y$ when $\forall x, f(x) \ge x$ and $Y$ is a finite partial-ordered set.

[Shuhao Song]

Sorry for English grammar errors.

[Yaël Dillies]

The preliminary lemmas should be separate PRs. You can ask github permission here. I am excited :smile:

[Shuhao Song]

Are there some automated tools to naming a theorem? I have lemmas called lm1, lm2, lm4 and so on...

[Shuhao Song]

Maybe GPT could help, it works well on pure language tasks. It writes better English than me :)

[Rida Hamadani]

#naming

[Shuhao Song]

Yaël Dillies said:

The preliminary lemmas should be separate PRs. You can ask github permission here. I am excited :smile:

See https://github.com/leanprover-community/mathlib4/compare/master...meow-sister:mathlib4:master, there would be 4 PRs: one for lemmas about List, one for lemmas about Walk, one for lemmas about iterations of function with $f(x) \ge x$, and one for main theorems.

[Yaël Dillies]

Sounds great!

[Shuhao Song]

https://github.com/leanprover-community/mathlib4/tree/meow-sister/BondyChvatal

[Shuhao Song]

@Yaël Dillies The pull request: https://github.com/leanprover-community/mathlib4/pull/15720.

[Yaël Dillies]

Ah you didn't read properly the contribution guidelines. You should not open PRs from forks, but from the mathlib4 repo itself. Sorry, I can't read