- November 8, 2025
Lean4 Macros for Implementing Custom Quantifiers
- August 29, 2025
Extracting Terms from Big Operators on Sequences in Mathlib
- April 23, 2025
A Meditation on Extending Inductive Types in Lean4
- April 23, 2025
A Simple Typeclass for Logic Formulae in Lean4
- August 6, 2024
A Basic Inductive Type Comparison: Rust, Lean, C, C++
- April 11, 2024
Formalizing The Singularizing Properties Problem
- March 18, 2024
Golfing Rozek's Lean4 Tutorial
- February 18, 2024
Proving the Correctness of Insertion Sort in Lean4