Hacker News: Jhsto

New comment by Jhsto in "Fermat's Last Theorem in Lean 4"

Jhsto — Fri, 04 Sep 2026 21:54:04 +0000

My anecdotal experience is that while LLMs are quite good at closing theorems given an LSP to inspect the proof-tree, they suffer from similar kind of problems with proofs as they do with bigger codebases in any language -- finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense). However, Buzzard has many times said that he wouldn't care how big the proof is and how ugly it would be, as long as there would be a proof.

New comment by Jhsto in "Rust SIMD on the GPU"

Jhsto — Tue, 11 Aug 2026 11:15:14 +0000

SPIR-V states its an int, float, vector n (where n <= 4) or a matrix (2..4 cols of vector n).

It does not necessarily mean the hardware can do 4x4x64 floating point operations in a single subgroup operation, but at least the programming model supports framing it that way.

MSI Pro B850-P WiFi Dasharo v0.9.0 Released

Jhsto — Fri, 31 Jul 2026 21:56:55 +0000

Article URL: https://blog.3mdeb.com/2026/2026-07-30-msi-pro-b850p-v090-release/

Comments URL: https://news.ycombinator.com/item?id=49129006

Points: 2

# Comments: 0

New comment by Jhsto in "Recursion is lying to you"

Jhsto — Wed, 29 Jul 2026 01:22:54 +0000

I've been writing a language around recursion schemes! Insofar it's just a library for Lean, but I wish to one day release it as an array programming language. I'm submitting a thesis in ~3 months, after which I'll be open-sourcing it.

New comment by Jhsto in "We have proof automation now"

Jhsto — Sun, 26 Jul 2026 22:19:29 +0000

As a meta-comment on the topic, something I have noticed is that there still exists confusion what it means to use theorem provers for projects -- the other day I read a tweet from Paradigm, a crypto-VC now seemingly AI-pilled. Some LP of theirs had made a Lean 4 formalization of the Ethereum's virtual machine. The tweet said this would have cost like $150k in API tokens ("would have", as in, I guess they get theirs for free), and took a week of inference time for an LLM to produce. I somehow got distracted to actually take a look at the code, which I found rather light on theorems. Nor did the project make use of Batteries or Mathlib which are arguably the one of the strongest motivation for me personally to use Lean4. That is, I generally rather rely on someone else getting the category theory and algebraic structures right, which then leaves me the proof obligation to show the correspondence with whatever toy I'm working on. Here I'm fine to use LLMs for proof search, very similar to how would I use a SMT solver. But what I have found is that the language models have to be really coerced into using these libraries, because otherwise the models much rather overfit and overclaim a solution with a 3 minute inference task rather than attempt to fulfill the proof obligations over 3 hours. And I feel nauseated when I need to convince the LLM (I use Claude) that filling the proof obligation is for "academic exercise" or because I'm coerced into doing so, because otherwise it will come up with reasons of its own why it does not want to do it. Now, this happens under the mental model in which I'm interested in finding equivalences with prior work. Many LLM generated Lean code reads more as if someone was interested whether X can be turned into a Lean 4 program, which is mostly yes, and that in general is a positive thing. But, if you are not interested in refinement types and theorems, why not just choose Haskell? The point is, I strongly sense that unless you have good questions to ask, then that's very evident in these languages. And, this is something the LLM won't help you -- if you don't impose a proof obligation for it, it certainly will not try to go the extra mile to conjure one for you.

New comment by Jhsto in "Vulkan Tutorial"

Jhsto — Thu, 23 Jul 2026 20:59:59 +0000

Another good tutorial: https://hoj-senna.github.io/ashen-aetna/

I used that to create my own Vulkan compute loader https://github.com/rivi-lang/rivi-loader

New comment by Jhsto in "Train sim created by just one person is being called the best ever made"

Jhsto — Thu, 09 Jul 2026 22:36:32 +0000

Anecdote, but I recall my friend saying he worked on freelancing assets to some train game and showed me some pictures of the said game. Unless there are more of these in existence, I think it was this.

GeForce Trading Cards: Series 1 Celebrates the Generations of GeForce

Jhsto — Thu, 09 Jul 2026 22:27:04 +0000

Article URL: https://www.nvidia.com/en-us/geforce/news/geforce-trading-cards-series-1-summer-of-rtx-giveaways/

Comments URL: https://news.ycombinator.com/item?id=48853206

Points: 1

# Comments: 0

New comment by Jhsto in "I Changed My Name"

Jhsto — Thu, 09 Jul 2026 22:18:12 +0000

I have this weird thing about a birthday -- for some reason, I was assigned a different birth date in NHS records in the UK compared to the one I have in my native Finland. I want to believe it has something to do with electronic systems transacting with different countries' systems (I noticed this difference soon after I exchanged my driver license) -- and I would have indeed born on a different day if it'd been the UK. But, I would assume this to be such a well-known issue with people who migrate, that it must just been just a typo. Doesn't stop me from believing though.

New comment by Jhsto in "Applied Category Theory Course (2018)"

Jhsto — Sat, 04 Jul 2026 10:59:09 +0000

Kiitos! My level is graduate, but part of the challenge with category theory is that some of the terms are quite unsuggestive. I feel that after seeing enough examples, I can start making more sense what some concept would be in Finnish, which helps me remember what was what and what it might relate to.

Edit: Also realized you're in Oulu, feel free to email me if you'd be up to meeting in-person to discuss these further!

New comment by Jhsto in "Applied Category Theory Course (2018)"

Jhsto — Sat, 04 Jul 2026 10:49:05 +0000

Thanks for the links! The first book seems very good (I already own the latter).

New comment by Jhsto in "Immich 3.0"

Jhsto — Fri, 03 Jul 2026 23:44:50 +0000

I think I dug my own grave by not being explicit that I thought S3 as a protocol and not the AWS product. :)

To elaborate a bit further, the S3 layer makes sense once you self-host S3 yourself. This allows clusterization of multiple hosts to offer redundancy in self-hosted setting -- for example, a friend of mine and I run S3 instances and "seed" each others' buckets for photo storage, but also for package manager (Nix). Having this kind of sane object storage just expands in use-cases, like with Matrix, etc., which all then inherit the clusterization hence redundancy for free.

The E2E encryption is also very useful when you are backing up or hosting photo galleries for friends and family -- because you cannot do metadata analysis on encrypted files, they have to do that on their own devices. This makes self-hosting much more "fearless" because I do not have to account for the fact that when/if my nodes are becoming a sauna-stoves for doing inference when someone dumps an album in.

The datasets that I have are terabytes. At some point it's just cheaper (accounting your time as free) to buy a 20tb drives and get yourself a runway for 5 years or more + space to do other stuff.

New comment by Jhsto in "Applied Category Theory Course (2018)"

Jhsto — Fri, 03 Jul 2026 23:32:47 +0000

As a programmer interested in category theory, I found this book a rather good balance between the abstract non-sense of CT and what I might actually use in programming. I wonder if anyone else has good books to recommend? I feel that the contents of the book remains a bit hard to appreciate in full unless you have ran into these concepts previously.

New comment by Jhsto in "Immich 3.0"

Jhsto — Thu, 02 Jul 2026 19:36:42 +0000

You can use https://ente.com/ (it's open-source). It also makes the seemingly much better decision of storing photos in S3.

New comment by Jhsto in "Bashblog – a single bash script to create blogs"

Jhsto — Sun, 28 Jun 2026 12:03:36 +0000

I'd presume it's quite common with NixOS. At least I don't have python linked to my environment. It might be different would I use the REPL, but I do not, so for me python is a program (or script) dependency, not something I need to carry around. It's actually quite common for many setup scripts to fail when python is not installed, but not all of them list python as a dependency either.

New comment by Jhsto in "AutoKernel: Autoresearch for GPU Kernels"

Jhsto — Wed, 11 Mar 2026 14:34:03 +0000

If I'd like to benchmark a new language / compile backend for LLM inference, what would be some good projects to try? If I'd start from tinygpt, what would make sense as the next step?

New comment by Jhsto in "Jolla phone – a full-stack European alternative"

Jhsto — Mon, 02 Mar 2026 14:59:25 +0000

Seems that Jolla C2 can run "close-to" mainline kernel: https://forum.sailfishos.org/t/mainline-linux-kernel-for-the...

New comment by Jhsto in "Xbox UI Portfolio Site"

Jhsto — Tue, 17 Feb 2026 09:54:53 +0000

I was able pull together a Halo 3 LAN party last year, although the "consoles" were Linux PCs and the game was the MCC edition (60fps instead 30). Split-screen was resurrected via mods. I bought some Microsoft gamepad receiver to bring Xbox 360 original controllers under Linux. Some people insisted they get to play on the original gamepad (otherwise it was a mixed bag of PlayStation and newer Xbox/PC controllers). I also realized that Halo 3 itself would have been old enough to drink with us!

New comment by Jhsto in "Mathematics for Computer Science (2018) [pdf]"

Jhsto — Fri, 09 Jan 2026 10:00:11 +0000

I got no particular book recommendation, but this book seems more about the numbers than relations -- maybe my PDF search is broken, but both 'type theory' and 'category theory' return 0 results. I would recommend to also look into those if you are interested in mathematics of computer science.

New comment by Jhsto in "Going immutable on macOS, using Nix-Darwin"

Jhsto — Fri, 02 Jan 2026 13:00:51 +0000

>I think where Nix shines isn’t “one laptop every 6 years” but when your environment needs to be shared or recreated: multiple machines, a team, or a project with nasty native deps.

I'd like to add the third thing, which is just iteration. It's very tricky to maintain advanced workflows even locally. I'd guess many won't even try to compose things that could work in combination (often self-hosted services), when they know they can't reliably maintain those environments.