Hacker News: Jaxan

New comment by Jaxan in "Rate limits on GitLab.com are changing"

Jaxan — Thu, 17 Sep 2026 16:50:43 +0000

Yes. A lot is not accessible if not logged in.

New comment by Jaxan in "Rate limits on GitLab.com are changing"

Jaxan — Thu, 17 Sep 2026 16:49:57 +0000

Doesn’t help with scrapers though. They use a unique IP for each query.

New comment by Jaxan in "Online Z3 Guide"

Jaxan — Thu, 17 Sep 2026 11:18:54 +0000

Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.

New comment by Jaxan in "A beginning for mathematics"

Jaxan — Tue, 15 Sep 2026 08:41:07 +0000

With human proofs, I have some trust in process behind it.

New comment by Jaxan in "A beginning for mathematics"

Jaxan — Mon, 14 Sep 2026 20:23:20 +0000

The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.

New comment by Jaxan in "Show HN: Art – draw one stroke, let symmetry complete it"

Jaxan — Thu, 10 Sep 2026 16:44:46 +0000

I looked in the AppStore for “symmetry draw”, and there are at least 10 such apps.

New comment by Jaxan in "Formalizing Fermat's Last Theorem"

Jaxan — Sat, 05 Sep 2026 05:48:44 +0000

Wouldn’t a lot already be in leans mathlib?

New comment by Jaxan in "Formalizing Fermat's Last Theorem"

Jaxan — Fri, 04 Sep 2026 19:41:57 +0000

Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)

New comment by Jaxan in "Formalizing Fermat's Last Theorem"

Jaxan — Fri, 04 Sep 2026 19:40:27 +0000

This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.

We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)

New comment by Jaxan in "We found a division by zero bug in FFmpeg with a vibecoded fuzzer"

Jaxan — Fri, 28 Aug 2026 06:22:34 +0000

I guess it’s submitted for the method rather than the result.

New comment by Jaxan in "Show HN: Make your logo extra bright on HDR screens"

Jaxan — Sat, 22 Aug 2026 20:19:17 +0000

It also depends on your screen brightness. In my case, if it’s set to maximum, there is no difference between SDR and HDR.

New comment by Jaxan in "Cave of the Crystals"

Jaxan — Fri, 14 Aug 2026 09:12:19 +0000

Absolutely amazing. I recently searched this and google images showed so much ai slop. I don’t get that, why do people prefer generic Disney style crystal caves above the actual photographs of this amazing cave.

New comment by Jaxan in "Dithered QR Codes"

Jaxan — Sun, 09 Aug 2026 16:29:17 +0000

The specification of qr codes says you should look only at the centres, iirc.

New comment by Jaxan in "Show HN: Reverse Minesweeper"

Jaxan — Mon, 27 Jul 2026 06:54:21 +0000

I know it as binairo, which I have seen in paper magazines. On Simon Tatham’s puzzle collection it is known as unruly: https://www.chiark.greenend.org.uk/~sgtatham/puzzles/js/unru...

New comment by Jaxan in "Show HN: Reverse Minesweeper"

Jaxan — Mon, 27 Jul 2026 06:50:57 +0000

This is very similar to “Mosaic” on Simon Tatham’s puzzle webpage. There it is noted that: “This game is variously known in other locations as: ArtMosaico, Count and Darken, Cuenta Y Sombrea, Fill-a-Pix, Fill-In, Komsu Karala, Magipic, Majipiku, Mosaico, Mosaik, Mozaiek, Nampre Puzzle, Nurie-Puzzle, Oekaki-Pix, Voisimage.”

https://www.chiark.greenend.org.uk/~sgtatham/puzzles/js/mosa...

New comment by Jaxan in "Stolen Buttons"

Jaxan — Sat, 25 Jul 2026 17:59:17 +0000

Oh this reminds me that we used to create buttons for navigation in flash!

New comment by Jaxan in "Blender 5.2 LTS"

Jaxan — Sun, 19 Jul 2026 14:01:32 +0000

Market size is different: everyone needs a mail client, but not everyone needs 3d modelling.

New comment by Jaxan in "Thunderbird Desktop settings research: what we learned from your feedback"

Jaxan — Mon, 13 Jul 2026 20:16:01 +0000

Hmm strange, I have never had a thunderbird folder in my home dir. I use thunderbird on Mac, Windows and Linux (Ubuntu).

New comment by Jaxan in "Counting ArXiv Delays"

Jaxan — Mon, 13 Jul 2026 20:12:37 +0000

You can also just put a paper on your website (or google drive). If arXiv isn’t working for you, why submit there?

Personally, i see no problem with delays, research takes longer than a few days. Reviews take a few weeks or months even.

New comment by Jaxan in "Vint Cerf, a “father of the Internet”, is retiring"

Jaxan — Sun, 12 Jul 2026 08:57:23 +0000

Which also shows there isn’t “one father”, multiple things (and people) had to come together.