-
Show, don't tell
A small reflection on showing something before naming it while teaching.
-
rintro and A ≠B
Using rintro to simplify derivations of A ≠B in Lean
-
Understanding the Suffices Tactic in Lean
A small pattern I noticed in Lean proofs that can be simplified using the `suffices` tactic.
-
Vibe coding
I found a complete program that GPT wrote for me, more than two years ago.
-
Formalizing Length Functions in Coding Theory
A brief discussion on the formalization of length functions, which are more than just a mapping from elements of an alphabet to natural numbers. They also need to satisfy a capacity bound condition.