Comment by jboggan
19 hours ago
Lol it should be, but it doesn't seem complete. Line 49 just says "sorry"
/-- Cubic bipartite three-vertex-connected plane graphs have a Hamiltonian cycle. -/ def MainStatement : Prop := ∀ (V : Type u) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.IsRegularOfDegree 3 → G.IsBipartite → Planar G → ThreeVertexConnected G → HasHamiltonianCycle G
theorem main : MainStatement.{u} := by sorry
In some cases they have a full Lean formalization; in others they just use it for the problem statement. Getting rid of that "sorry" means you've proved the statement. I'm not a Lean expert but it reads pretty clearly as the original conjecture (though the definition of PlaneEmbedding seems quite involved!).
I think this just has to be the problem statement, there's several lemmas I would expect to see in there. Granted I know very little about Lean but it seems like the question and not the proof outlined in the paper.
They are using a Lean tool where you separately state your theorems with `sorry` and then prove them elsewhere. The tool checks that all sorry's are covered. This is so the AI doesn't need to edit the specification of the theorem statement.
2 replies →