Unnamed Website

Since Lean isn’t a very popular programming language (yet), it doesn’t have much support in KDE Plasma.

For the past two years, this site has been hosted on SIPB’s amazing XVM service.

“MIT Athena: Not Dead Yet”, they said back in 2008. 18 years later and 42 years after the start of Project Athena, somehow Athena is still (barely) alive and kicking, thanks to Nixathena!

Lean is an incredibly awesome programming language, as I’ve mentioned many times before on this blog.

It’s that time of the year again: April Cools!

You might remember my post last year about lazy infinite lists in Lean, back when I didn’t know how to write Lean.

“A monad is a monoid in the category of endofunctors, what’s the problem?”

Inspired by The Evolution of a Scala Programmer.

Typst is a typesetting system similar to LaTeX.

Kublai: sevglzioelkehcnwezshieoinkosy.ezwslegyoegaaese.kzevglezwsleakclxeliyziyniq Uh, are you OK, Kublai?

What is cosh(List(Bool))?

Four years ago, I installed every Arch Linux package (and someone else tried the same crazy experiment with Alpine Linux).

Kublai: BOO!!

Kublai: Hiiiii!!

In this post, I’ll explain how to replace the hinges on the Lenovo ThinkPad X1 Yoga Gen 6 convertible laptop, since I couldn’t find any guides online about it.

There’s currently an ongoing project to formalize Fermat’s Last Theorem in Lean, which will probably take many years to finish.

Last week, I visited Hong Kong, Macau, and Shenzhen, so here are some random photos from the trip.

Lean is a modern programming language that happens to also be a proof assistant.

One of my first blog posts is about a cool double summation identity: \[\sum_{n=2}^{\infty} \sum_{p=2}^{\infty} \frac{1}{n^p} = 1\] The pencil-and-paper version of the proof is short and sweet, so I thought it’d be a nice exercise to formalize it in Lean.

I lived in St.