- August 27, 2026
The Three Types of FOND Planning Policies
- February 20, 2026
What is f(x) ≤ g(x) + O(1)? Inequalities With Asymptotics
- November 8, 2025
Lean4 Macros for Implementing Custom Quantifiers
- August 29, 2025
Extracting Terms from Big Operators on Sequences in Mathlib
- August 17, 2025
Status Page Theater
- April 23, 2025
A Meditation on Extending Inductive Types in Lean4
- April 23, 2025
A Simple Typeclass for Logic Formulae in Lean4
- February 2, 2025
Emulating Rust's Result and ? in Jai with Metaprogramming
- December 14, 2024
A Transcription of John McCarthy's Czechoslovakia Visit Letter
- December 12, 2024
Speeding Up Collatz Iteration With Inline Assembly
- August 6, 2024
A Basic Inductive Type Comparison: Rust, Lean, C, C++
- June 24, 2024
Embedding, Jai, and Joy (Jai Part 2)
- June 23, 2024
Simplicity, Jai, and Joy (Jai Part 1)
- June 11, 2024
Inference Rules in Peirce's Alpha Existential Graphs (Part 2)
- April 11, 2024
Formalizing The Singularizing Properties Problem
- March 29, 2024
The Law of Excluded Middle Does Not Imply the Axiom of Choice
- March 18, 2024
Golfing Rozek's Lean4 Tutorial
- February 18, 2024
Proving the Correctness of Insertion Sort in Lean4
- January 4, 2024
Worldbuilding Formal and Aesthetic Magic Systems
- November 3, 2023
Anticode: A Good Minimalist Code Of Conduct