Three LLM Trends Today Posted on 2026-06-08 by ubikium About ten years ago, I was at the undergraduate school. One of the course work was to train a CNN (Convolutional Neural Network) for the MNIST dataset. I trained it on my laptop. Just yesterday, I created a new account in my ledger: “expenses:ai”, since I have to start paying for AI for my personal usage. In this post, I’m writing down some…
Process Theater Posted on 2026-03-05 by ubikium Recently a colleague of mine introduced “ Conventional Commit ” to an internal project which surprised me when I saw the CI failure. I don’t believe the creators of such “spec” have bad intentions. It’s just something that’s easy to be abused for a use case different from the one that it has intended. I’m even more surprised when I asked if this can…
Having a theory of your program Posted on 2025-12-18 by ubikium The problem of not having a theory of your program is that you can only have a theory of your program. However, having a theory of your program can only give you a theory of your program and nothing more.
Converting math-heavy LaTeX to HTML with Pandoc Posted on 2024-12-20 by ubikium Recently there’s a need to convert a math-heavy LaTeX document to HTML. Of all the tools I tried, Pandoc wins out as it’s the only one that didn’t choke on macros. It generated a surprisingly decent output and offered great customizability. In this post I’ll talk about the general setup and some tips on how to extend…
The Limitation of Open Source in its Libertarian Root Posted on 2024-05-05 by ubikium Or how people learned to start worrying and fear the bomb. A recent controversy brought up some deep questions about the nature of free & open source software movement (referred to as open source in this article). The details are not important for our purpose. Let’s just say there’s an open source community. At a…
How to read Lean 4 source code with LSP support Posted on 2023-12-10 by ubikium The problem The Lean 4 source code is a fantastic learning material to read. Previously I just picked a file and opened it with my editor, which was set up to use lean.nvim , and it just worked, with all the infoview and jump to definition stuff. But recently, after rebasing on master , the editor errored out with the…
Rainsea Radio: An AD Blocking Monitor Posted on 2023-09-10 by ubikium Today’s Rainsea Radio interview features the creator of a controversial startup, ClearUrGlass. People have described that the startup’s business is to destroy all other tech companies’ business, as its product, the CUG-1 smart monitor, automatically detects and remove ads from screen. The creator, a young and energetic Estonian…
let ← is not a definition Posted on 2023-08-30 by ubikium Or the deceptive appearance of the do notation. Proof is cheap. Show me the proof. Does this function terminate? def f (xs : List Nat) : Except String Nat := do let tail ← do match xs with | [] => Except.error "empty" | _ :: tail => Except.ok tail f tail Before you answer, I should note that this pattern do come up in real problems. This…
Use highlightjs version 11 for Hakyll Posted on 2023-08-29 by ubikium So the other day I tried to add syntax highlighting for a new language to this blog. Hakyll does support syntax highlighting and my previous setup also features a self-hosted pack of highlight.js . Previously they were somewhat working together, side by side. That is, whatever code I threw into the fenced block usually gets…
Tips and Reviews of The Little Prover Posted on 2023-08-24 by ubikium Similar to my last post which gives some tips and reviews of The Little Typer , this post will do the same thing, but for The Little Prover . Who is this book for? This book teaches theorem proving over recursive functions using induction. Suppose you want to prove a theorem related to a function. A sensible approach is to use a…