← Feed

Posts

• View post

  New blog post about the logical model for floating-point numbers that will be part of Lean 4.33: https://juliahimmel.de/blog/float-qanda/

• View post

  I just found out that the tram ride to my dance classes is between 22 and 23 minutes. You know what that means.... https://open.spotify.com/track/44HjyYf1lYuO7oXRusudHN1

• View post

  New blog post titled "An Underappreciated Lean Feature": https://juliahimmel.de/blog/an-underappreciated-lean-feature/

• View post

  I don't have a lot of reach on here, so boosts would be greatly appreciated. I'm looking for someone to join my team at the Lean FRO as a metaprogrammer with a view towards library quality. I'm working toward a future in which ITPs are a joy to use productively for mathematics and software verification. I believe that to get there, we need to get a lot better at building libraries that are complete, consistent and scalable, and a key factor in that will be to have excel...

• View post

  Just had my first Spekulatius of the 2026-2027 christmas season!

• View post

  Thought I had just discovered my first LLVM bug while working on the Lean runtime, but someone beat me to it: https://github.com/llvm/llvm-project/issues/217376 The good news is that the fix is already released, so I'm not blocked on the work I'm actually supposed to do, but I wouldn't have said no to the experience of reporting a bug to LLVM either 🙂

• View post

  Always good to see something you've worked on in an OpenAI misalignment report... lol https://alignment.openai.com/misalignment-reports/exposing-a-github-token-in-a-public-repository/ https://github.com/leanprover/lean-eval/pull/137

• View post

  I have a theory for the difficulty mystery: Problem 757, like many other PE problems, has the property that you can just brute force the first few terms of the sequence and then plop them into OEIS to get some major hints or possibly a full solution. Personally I would never do this because it takes most of the fun out of these problems, but I know that a lot of people consider OEIS fair game.

• View post

  Spoiler-free review of #ProjectEuler problem 539 (Odd Elimination): I really liked this one, it's not too difficult but a lot of fun to work out on pen and paper. You can *almost* solve it entirely without a computer but the numbers get a bit large. I solved it on my phone (might be the first one I did without a computer?) and accidentally called the solution while trying to copy it out. Recommended: https://projecteuler.net/problem=539

• View post

  Spoiler-free review of #ProjectEuler problem 772 (Balanceable k-bounded partitions): not my favorite problem; it's easy for all the wrong reasons and I was almost a bit upset when I saw the green checkmark. https://projecteuler.net/problem=772

• View post

  Spoiler-free review of #ProjectEuler problem 153 (Investigating Gaussian Integers): this is a nice medium-difficulty problem. You don't need to know much theory (the things I remembered from my elementary number theory course 9 years ago were certainly sufficient, or you can read the "basic definitions" section of the Wikipedia article without getting any spoilers), but there are some nice insights to be figured out. Recommended: https://projecteuler.net/problem=153

• View post

  I like short stories because they allow you to do interesting things, thematically and linguistically, that would not work at the scale of a novel. The short story collection 'Furies' (2023) has many great examples of this. I particularly enjoyed 'Wench' by Kristy Logan. Highly recommended if you can get your hands on the book!