Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by trissim on Thursday January 08, 2026 @02:32AM (#46538303)

You only read the 37 lines in SSOT.lean and stopped. It's the entry point that defines DOF=1 so other files can import it. The actual proofs are in Foundations.lean (364 lines - timing trichotomy, causality), Requirements.lean (derives the two necessary language features), Completeness.lean (mechanism exhaustiveness), Derivation.lean (the uniqueness proof that achieves_ssot m = true iff m = source_hooks), Coherence.lean, CaseStudies.lean, LangPython.lean, LangRust.lean etc.

~2k lines total across the lean files. Zero sorry. Run grep -r "sorry" paper2_ssot/proofs/ if you don't believe me.

"Unfolding the definitions they say x=1 => x=1" applies to three sanity lemmas in the scaffolding file. It's like reading __init__.py and concluding the package is empty.

[ Parent | on HN ]

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by BalinKing on Thursday January 08, 2026 @02:33AM (#46538310)

See my other comment—LangRust.lean is the same way.

EDIT: Just skimmed Completeness.lean, and it looks similar—at a glance, even the 3+-line proofs are very short and look a lot like boilerplate.

[ Parent | on HN ]

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by trissim on Thursday January 08, 2026 @02:39AM (#46538375)

Interesting that you're using em dashes in your comments. Those require Alt+0151 or copy-paste. Glass houses.

[ Parent | on HN ]

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by dwb on Thursday January 08, 2026 @03:14AM (#46538601)

And Option-Shift-Hyphen in macOS, which is easy if you know it. And a press and hold on a hyphen on iOS, which is discoverable, even.

[ Parent | on HN ]

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by BalinKing on Thursday January 08, 2026 @12:32PM (#46543823)

Yeah, I'm on macOS (although even back on Windows, I used to use the Character Map all the time).

[ Parent | on HN ]

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by trissim on Thursday January 08, 2026 @01:16PM (#46544426)

Fair, the em dash comment was a cheap shot. Withdrawn.

The substantive point stands: you've now "skimmed" multiple files, called them all "boilerplate," and haven't engaged with the actual proof structure. The rebuttals section addresses "The Proofs Are Trivial" directly (Concern 9).

At some point "I skimmed it and it looks trivial" stops being a critique and starts being "I didn't read it."

[ Parent | on HN ]