-
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.
-
Using numbers, real numbers, in Lean
Having a calculation with real numbers in Lean is not as straightforward as it seems. I'm sure I'll learn better ways to do it in the future, but for now, I want to share how I solved this problem.