-
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.
-
Induction and rfl
A subtle detail in the use of induction and rfl
-
Lean snippets
Beginning a collection of Lean snippets