Hacker News Reader

Comment by jboggan | Hacker News Reader

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

View on HN

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.

Ah, cool. I'm still learning Lean - is there somewhere else in the repo with the Lean specification of the cycle construction for the full argument?

the json file next to the problem statement in lean says the solution starts here: https://github.com/openai/math/blob/main/lean/OAI/Combinator...

the proof is probably split over the constructions in the whole directory.

Aha, thank you, this makes more sense now.

Reply on news.ycombinator.com