← 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've been getting back into #ProjectEuler lately, and I will be posting short spoiler-free reviews of some of the problems in the hope that they will make you interested enough to try them yourself.

• 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

  Spoiler-free review of #ProjectEuler problem 349 (Langton's Ant). I enjoyed this easy problem very much. Do not, under any circumstances, search the internet for the term "Langton's Ant" or you will be spoiled and the problem will be ruined for you! Recommended: https://projecteuler.net/problem=349

• View post

  Spoiler-free review of #ProjectEuler problem 757 (Stealthy Numbers): this is a nice little problem with a nice solution. It made me feel quite stupid because it took me a while to solve it despite its difficulty rating of 3/39. I don't really understand these difficulty ratings. I know they are computed from the solve statistics, so they are "objective", but I just cannot see how 349 is an 11/39 if 757 is a 3/39. Recommended: https://projecteuler.net/problem=757

• 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!