- October 14, 2026
def∇: An inductive∇ Macro
- October 8, 2026
def∇: A Drop In def∇
- October 7, 2026
def∇: An APL-Style Self Reference Macro for Lean4
- 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