Show HN: A lean formalization of From Linearity to Borrowing
By empath75 · 2026-10-02 · 1 points · 0 comments
https://github.com/empath-nirvana/bolo-formalization
This is a full mechanization of the From Linearity to Borrowing paper in Lean https://dl.acm.org/doi/10.1145/3764117 The work was almost entirely done by Claude over the course of 3-4 weeks. It follows the paper and technical supplement as closely as I c…
Open the full discussion on BetterNews