Doubt regarding the status of The Bondy-Chvátal Theorem

Stream: graph theory

[Kartik]

Hello everyone, I wanted to work on Dirac's theorem on hamiltonian cycles but I saw in another post that The Bondy-Chvátal Theorem which is a general version of what I wanted to prove is already done.

https://github.com/leanprover-community/mathlib4/pull/15720/files

The code is there on Github but I can't find the theorem on https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Hamiltonian.html

Can anyone please clarify the situation?

[Kevin Buzzard]

The PR you look to is still open, depends on other open PRs at least one of which is apparently not done in the correct generality according to comments on the PR, and has merge conflicts. I'm particular it's not in mathlib master and is not even ready for review. Looks to me like before embarking on another proof there should be a discussion on the mathlib-acceptable route.

[Matthew Coke]

@Kevin Buzzard I'm all for methodology discussions. I think that creating documents to describe processes and locations to newcomers (like myself) would be a good idea. I think a "tour guide" would be a good thing to create

[Kartik]

Thank you @Kevin Buzzard

[Kevin Buzzard]

Yeah this question also made me think about maybe creating some document. I think the key fact is that if it compiles and is a fully correct proof of a theorem then this certainly does not mean that the work is ready for mathlib. This particularly applies to AI-generated proofs which in essentially all cases are not ready for mathlib. The three main issues which are problematic are: (1) proof not in the correct generality for mathlib (eg should be proving a far stronger theorem, which in some cases might be much harder to do); (2) result not suitable for mathlib at all (eg because it's not a topic mathlib is interested in covering) and (3) unidiomatic proofs (this is often the case with AI proofs which are typically 10x as long as an expert-written proof).

[Matthew Coke]

@Kevin Buzzard workflows come to mind. I worked with Salesforce for awhile but there are lots of other ways to create too