Comment by Daneel_
18 hours ago
It might have been updated. Is this the lean? https://github.com/openai/math/blob/main/lean/docs/180.md
18 hours ago
It might have been updated. Is this the lean? https://github.com/openai/math/blob/main/lean/docs/180.md
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.
3 replies →