Ore's Theorem

Stream: PR reviews

[SHAO YU]

I have submitted a PR that proves the classic Ore's theorem#34481 in graph theory. Currently, the proof exceeds 4,000 lines. I look forward to more people participating to simplify it and make it more compliant with Mathlib standards, so that it can be merged into Mathlib as soon as possible.

[Johan Commelin]

Wow! Is that a record for longest-Lean-proof-ever?

[Martin Dvořák]

Of course it isn't the longest proof in Lean.

[Martin Dvořák]

The question is whether maximal_path_extends_or_hamiltonian is the longest atomic proof written in Lean.

[Martin Dvořák]

set_option maxHeartbeats 200000000000000

[Ruben Van de Velde]

It's more than one theorem, but there's 500+ line proofs in there

[Violeta Hernández]

The Wikipedia proof for this is a single paragraph. I don't think this should take more than 200 lines or so.

[Violeta Hernández]

AI is good at proving theorems, but it's not good at proving them well. If you want to PR this sort of material to Mathlib, you have to make sure you understand the argument the computer is making, and trim all of the extra fat.

[Snir Broshi]

Violeta Hernández said:

The Wikipedia proof for this is a single paragraph. I don't think this should take more than 200 lines or so.

That's a slick proof, but I think 200 is far too low for non-trivial graph-theory in Mathlib right now (unless you're counting each theorem individually).
For example, IIUC the Wikipedia proof uses this at the start (at "let x and y be any two non-adjacent vertices in H") :

theorem IsHamiltonian.top_of_three_le_card (h : 3 ≤ Fintype.card α) : (⊤ : SimpleGraph α).IsHamiltonian := sorry

Here's how my attempt ended

Tried and failed with various induction principles, such asFintype.induction_empty_option.
Instead let's prove that ⊤ has a Hamiltonian path (not a cycle) which is true for any [Nonempty α], then we'll close it to a cycle afterwards.
Ideally I'd want to use ofPathGraph from #34171 and .map it to the ⊤ graph, but to avoid extra imports lets let rec inline.

import Mathlib.Combinatorics.SimpleGraph.Walks.Maps
namespace SimpleGraph

/--
info: PANIC at Lean.EnvExtension.modifyState Lean.Environment:1399:17: `asyncDecl` `SimpleGraph.foo.f` is outside current context SimpleGraph.foo
backtrace:
---
warning: declaration uses `sorry`
-/
#guard_msgs in
lemma foo : True := by
  let rec f (n : ℕ) : Walk ⊤ 0 (Fin.last n) :=
    match n with
    | .zero => .nil
    | .succ n => .cons Fin.zero_ne_one <| f n |>.map ⟨Fin.succ, Fin.succ_inj.not.mpr⟩
  sorry

Nope.

Not that I'm in any way justifying the PR above, but I think 1,000 lines is a more reasonable bound.
btw if anyone can easily prove this small theorem I'd love to know.

[Violeta Hernández]

It seems to me that we're missing a function to construct a walk from a Fin (n + 1) → G, or a cycle from a Fin n → G. Then the Hamiltonian path in question would just be given by Fintype.equivFin G.

[Vlad Tsyrklevich]

#15720 is an abandoned PR proving Bondy-Chvatal which is a generalization of Ore. It's +900, but 1.5 years old so unclear to to me what it would be with the current API, grind, and further review. I noticed scrolling through that there are at least a few API lemmas in there that I recognize having contributed since then, though half of the PR is specific to the main theorem.

[Johan Commelin]

@Vlad Tsyrklevich thanks for pointing that out! Do you also want to cross-link the PRs?

[Vlad Tsyrklevich]

I'm not sure what 'cross-link' means. You mean just mention #15720 in a GitHub comment on this PR?

[Johan Commelin]

Yup, just copy this zulip comment to a github comment on #34481. Then the other PR will also be notified.

[Vlad Tsyrklevich]

Snir Broshi said:

theorem IsHamiltonian.top_of_three_le_card (h : 3 ≤ Fintype.card α) : (⊤ : SimpleGraph α).IsHamiltonian := sorry

I started working on this and quickly got bogged down in induction arguments. This feels like something where it would be great to have a Walk.ofList. Then you pass [0, ..., card - 1, 0] mapped across the Fintype equiv and prove adjacency. Hopefully proving it's a path and a cycle would then be trivial from having the support explicitly specified (but I'm probably oversimplying.)

EDIT: #34799

[SHAO YU]

I have re-proven my theorem and uploaded it. I have extracted some of the lemmas into separate lemmas to better align with Mathlib's standards. Alternatively, I also see PR #15720 (although this PR has been abandoned), and my proof approach is based on the idea that a graph satisfying Ore's condition must contain a Hamiltonian path, from which both the Hamiltonian path and Hamiltonian cycle are constructed. Comparing the two PRs, do you think it is still worthwhile for me to persist in revising my proof with the expectation of merging it into Mathlib?