News for hackers. Stuff that matters.

A comment on Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection.

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by hanslub42 on Thursday January 08, 2026 @02:51AM (#46538452)
All the heavy lifting is done by the comments. For example: theorem dof_gt_one_inconsistent (dof : Nat) (h : dof > 1) dof ≠ 1 (in Basic.lean) is the well-known fact that any number > 1 is unequal to 1.

But the comment states: DOF > 1 implies potential inconsistency. Inconsistency of what? Lean doesn't know, or care....

[ Parent | on HN ]
Re:Show HN: Lean4 proof that SSOT requires definition-time h... by trissim on Thursday January 08, 2026 @03:35AM (#46538730)
Fair point. I've added Ssot/Inconsistency.lean (zero sorry) which formalizes inconsistency as a Lean Prop, not a comment.

It proves ssot_required: if you need to encode the fact (DOF >= 1) and guarantee all configs are consistent, then DOF = 1. Also formalizes independence and oracle necessity (valid oracles can disagree -> resolution requires external choice).

The mapping to real systems still requires interpretation,but so does every formalization. The contribution is making assumptions explicit and attackable.

[ Parent | on HN ]