Ubikium's blog

Three LLM Trends Today Posted on 2026-06-08 by ubikium About ten years ago, I was at the undergraduate school.

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.

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.

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.

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.

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.

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.

let ← is not a definition Posted on 2023-08-30 by ubikium Or the deceptive appearance of the do notation.

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.

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.