minihol. Scala
jct-reformalization. A reformalization, in Lean 4, of the proof of the Jordan Curve Theorem, adapted from the HOL Light proof by Thomas Hales.