Chris Henson

I wrote a short blog post "The Interplay Between Metaprogramming and Computation in Lean": chrishenson.net/posts/2025-0...

Yeah it doesn't always work out. To get an extremely homogeneous deck you really need DNA (make a copy if first hand is high card) with Blueprint(s).

Sometimes I like to try ending up with a tiny deck of all the same card. Often I'll speculatively go for King/Queen for the most powerful jokers, though that does make facing The Plant a bit risky. Especially with higher stakes and antes in endless mode there's a fair amount of luck

The LaTeX this exports uses tikz-cd, but it is certainly much easier to use than writing it by hand.

I've used quiver for my upcoming candidacy exam paper and highly recommended it. Easy to use, and every diagram comes with a link that encodes the diagram. Very nice feature for making edits later.

Since it was only triangles for part 1, I did possibly the most inefficient solution of going out three nodes from each key and checking when the start/end was the same, then a bunch of sorting and erasing duplicates.

(Going to leave part 2 for when I finish my port of the pathfinding crate)

A few interesting finds at used bookstores today.

My lack of Advent of Code posting is because I've gotten completely sniped into porting Rust's pathfinding crate to Lean, including an implementation of insertion-order preserving hashmaps. If I get it finished and cleaned up over the holiday, I'll be sure to share!

Proving that negative axioms don't break canonicity In Negative consistent axioms can be postulatedwithout loss of canonicity, the authors show that if $\lnot P$ is a consistent axiom with MLTT, then MLTT+$\lnot P$ still has canonicity of $\mathbb N$.

I wanted to answer this but was too lazy and got scooped!

proofassistants.stackexchange.com/q/4526

It's a cool way to use canonicity to give *conservativity* results: a bunch of stuff to add to your logic without making it less trustworthy.

This is one of the first applications of canonicity!

I am so glad Drexel decided to keep around free SEPTA for (some) PhD students so I don't have to think about this lol

Eh, I see what you mean, but I think part 1 was meant as a hint of how you could get the correct time programmatically even if you didn't print anything out. I think checking for some measure of density is pretty intuitive.

Feels a bit odd to post this here too, but I added a short blog post to my site about the ways Twitter has affected my life and career.

chrishenson.net/posts/2024-1...

It seems relatively common in Lean too. People just usually put it above the definition so I didn't realize it worked for any expression

Putting an `open` inside a definition is interesting. It makes sense but I'd never seen it.

Funnily enough, some people seem to really dislike the days with a visual component. After searching manually for a bit, I made a guess that we wanted the frame with the most dense lines and that worked.

Here is my beautiful unicode Christmas tree. (Hopefully the image blurs, they really should add a spoiler tag)

advent-of-code/2024/lean/AoC/Day14.lean at main · chenson2018/advent-of-code Contribute to chenson2018/advent-of-code development by creating an account on GitHub.

Day 14 of #AdventofCode in Lean: github.com/chenson2018/...

Nothing too notable, except for being one of the days with a visual element that sometimes generates a bit of controversy.

Oh lol, that makes more sense. Posting a link a day for AoC certainly skews the results...

I'm convinced it also includes the text of usernames when you reply, because mine ("chenson") appeared in my cloud lol

advent-of-code/2024/lean/AoC/Day13.lean at main · chenson2018/advent-of-code Contribute to chenson2018/advent-of-code development by creating an account on GitHub.

Day 13 of #AdventofCode in Lean: github.com/chenson2018/...

Just some algebra today. I spent a while fiddling with Diophantine equations, I was disappointed they weren't needed.

One thing I miss is defining a notation at the same time as a typeclass. You sometimes end up with typeclasses whose sole purpose is a one-off notation, which arguably isn't great.

But in general, I love Lean's system of syntax/elaboration. It just feels "right" to me, if a bit arcane at times.

One thing that eluded me was proving termination for the mutually recursive memoized function. Past that, I think you could maybe write a metaprogram to generate these from regular recursive functions, but that's a bit past my ability level.

advent-of-code/2024/lean/AoC/Day11.lean at main · chenson2018/advent-of-code Contribute to chenson2018/advent-of-code development by creating an account on GitHub.

Day 11 of #AdventofCode in Lean: github.com/chenson2018/...

One day lag here because I really got into this problem! I defined memoization as a state monad, along with a memoized map function that folds a hashmap over a list.

Out of curiosity I went and checked my wabbit repo, 17 clones there. About half in the code for environments, half in the LLVM, and two in the parser for peeking.

So would Lean's namespaces fall under this, where for instance you can write either `List.map xs` or `xs.map`?

I tend to like it in pipes, especially since they also open namespaces, e.g. `|>.map`. Insensitivity to argument order is nice too.

I love seeing the language distribution in my Advent of Code repo change over the years

advent-of-code/2024/lean/AoC/Day10.lean at main · chenson2018/advent-of-code Contribute to chenson2018/advent-of-code development by creating an account on GitHub.

Day 10 of #AdventofCode in Lean: github.com/chenson2018/...

Very straightforward, not much to say. One of those days where part two was one a one line change from part one.

Doing your compiler class in Rust was a lot of fun, glad to see others will have a similar experience!

Also part two does a lot of reversing of lists, but this is still fast enough (~3.5s for both parts) that I didn't really give it much thought

advent-of-code/2024/lean/AoC/Day09.lean at main · chenson2018/advent-of-code Contribute to chenson2018/advent-of-code development by creating an account on GitHub.

Day 9 of #AdventofCode in Lean: github.com/chenson2018/...

Nothing conceptually difficult, but lots of bookkeeping here that took a while to get right and could probably be a bit cleaner.