Nazrin: A Transposing Atomization Algorithm
Searching for treasure?
The Chrysoberyl
Latest posts
Announcing the release of Prismriver.lean
A Music Formalization Library in Lean 4
Self-Host Concourse CI with NixOS
Parametric Cosplay Design - Toyosatomimi no Miko (豊聡耳 神子)
undefined
Interlude: Fixture ACME Testing a NixOS Configuration
No compromise
Topological Intersection Stackup Diagrams
Sewing for the Differential Geometer
Cosplay Special Effects in Blender
You can do it too
Supersinographic MATP Terminologies / 機械定理証明之超漢文語彙
A Reproducible Nix-Forgejo Server
We Must Develop White-Box Artificial Intelligence
The Future Directions of MATP
At ICML'25 AI4Math workshop
Parametric Cosplay Design - Yasaka Kanako (八坂 神奈子)
First step towards declarative cosplay design
A Course in Lean 4 at Stanford University
The Perfect Math Class
Information Sign: Satisfiability Modulo Theory
CDCL and Quantifiers
Information Sign: Search and Coupling
Metavariables, Coupling, and Formal Proofs
Singularity for the Impatient
Announcing the Release of Pantograph and PyPantograph
A machine-to-machine proof assistant interface
Cooking: Yuzu Ice Jelly
undefined
Unofficial Lean Nix Flake
Why?
Lowering the Barrier of Entry of Cosplaying
Is it possible?
New Website
Overhauling the website for presentation and clarity
Hyprland/Swayfx and Eww Desktop Environment
Announcing the Release of Pantograph v0.2.13
A machine-to-machine proof assistant interface
Trillium Devlog: Calling Lean from Rust
How I got into Computer Science
An unbelievable story
Trillium Devlog: A Rust development environment in Nix
LatexMk relative directory compilation hook
A method for finding project root in emacs
Hyprland/Waybar Desktop Environment
The Philosophy of Colours
How colours impact the cognitive load of the reader
Cooking: Sichuan Fried Pork
Sichuan Style Fried Pork adaptable to frying tofu
Cooking: Curry
Japanese style flank plate, carrot, and potato curry
Doom Emacs
Creation of the Stanford Photography Club
Reloaded