Add work-in-progress Lean formalization - #165

Open

daira wants to merge 8 commits into

Commits on Jul 14, 2025

Add work-in-progress Lean formalization.
daira
committed
0d2c8e5
Merge `lca_same_length_{left,right}`, and minor cleanups.
daira
committed
5e3f2bb
Crosslink.lean: take the params explicitly.
daira
committed
1166cc5

Commits on Aug 16, 2025

Doc improvements.
daira
committed
2326b96
Simplifications; only depend on NoCollisions where we need to.
daira
committed
140bb35
Fix a bug found by attempting the proof of `lca_unique`.
daira
committed
a2243ae
Finish `LCA.lean`.
daira
committed
7b78794

Commits on Mar 8, 2026

Apply suggestions from code review

daira
and
oxarbitrage
authored
98d0f5a