Mathematics and programming, with a proof assistant at hand.
- Collatz, but stop at the drop: two papers and their Lean 4 / Mathlib formalization. The question is not whether every start reaches 1, but whether every x > 1 eventually falls below itself.
- rud1: a mostly functional programming language inspired by pari/gp, with a Lean 4 prototype as its reference.
Netherlands · ISOLUTION B.V.

