HN Explorer

trissim

↗ HN profile [ 37.7 ms ] full profile
Karma
0
Created
()
Submissions
0
  1. Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection (zenodo.org)

    I formalized the Single Source of Truth (SSOT) principle in Lean 4 (~2.1k LOC, zero sorry) and proved two core results: Structural SSOT is achievable only when a language provides definition-time hooks and runtime…

    10 points 6
  2. Show HN: Knowing What Matters is coNP-complete (Lean 4 formalized) (zenodo.org)

    We prove that identifying decision-relevant coordinates in a decision problem is coNP-complete. Finding the minimum sufficient coordinate set is also coNP-complete. Formally: given state space S = X_1 × ... × X_n and…

    2 points 0
  3. Show HN: Proof that any fixed-axis type system fails for some domain (Lean4) (zenodo.org)

    I formalized a proof that the structural vs. nominal typing debate can't be won: any fixed-axis type system necessarily fails for some domain. The core result: for a type system with fixed axes (like structure,…

    3 points 0
  4. Proof that any fixed-axis type system fails for some domain (formalized in Lean) (zenodo.org)
    2 points 1