HNHacker News
TopNewBestAskShowJobs

Someone

33,683 karma · joined February 8, 2008

submissionscomments
Someone··on Classification of Finite Simple Groups Formalized in Lean
_If_ you have formalized a provable theorem in Lean, a simple bread-first search can prove it. It will take lots (and lots, and lots, and lots…) of time, though (https://en.wikipedia.org/wiki/General_Problem_Solver).

LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.

Someone··on I still teach OpenGL ES 3.0
At least partly, it’s a form of choice-supportive bias (https://en.wikipedia.org/wiki/Choice-supportive_bias).

Your mind cannot live with the idea that you spent many, many hours learning an ugly API, so it makes you think it is better than it is.

Someone··on The Exponential Time Hypothesis Is False [pdf]
> The fact that other math problems are bulk solved yet nothing from cryptography was released/published as solved could be a strong indicator that "all modern public key based cryptography" could have been at risk.

“Could be”, but I think the correct way to describe it is “the general public doesn’t know”. It could be any of

- they tried very hard without finding weak spots

- they tried for a while, and gave up because the LLMs didn’t even produce leads

- they tried, found something and kept it for themselves

I think the first is not unlikely. Before LLMs, the likes of the NSA must have looked really hard into these problems, and IMO it’s not likely they found something substantial (if they did, their counterpoints in other large countries likely would find it, too, and some of them would have used that knowledge)

Someone··on How to grow a cacao tree at home (2024)
More likely from an intermediary, possibly one from the Netherlands. https://www.expatrepublic.com/netherlands-largest-cocoa-expo...:

“For most people, tulips, windmills, and bike lanes spring to mind when they think of the Netherlands. But most people would be surprised to learn that the Netherlands ranks first in the world as an exporter of cocoa products, recently overtaking neighboring Germany.

The Netherlands recorded cocoa exports of 12.4 billion euros in 2025”

I would guess that’s a holdout from colonial times. Indonesia used to be a Dutch colony up till world war two. Might even date back to when there was a Dutch colony in Brazil (https://en.wikipedia.org/wiki/Dutch_Brazil), but that page doesn’t mention cocoa, and I wouldn’t even know whether there was cocoa in Brazil at the time.

Someone··on Microsoft offers mass buyouts for roughly a quarter of its workforce
I assume you pronounce that X as the X in Mexico.
Someone··on Blaise Pascal invented fixed route public transport (2024)
https://en.wikipedia.org/wiki/Trekschuit:

“Trekschuit (Dutch pronunciation: [ˈtrɛksxœyt] ⓘ; lit. 'tug-boat', i.e. 'tugged boat') is an old style of sail- and horse-drawn boat specific to the Netherlands, where it was used for centuries as a means of passenger traffic between cities along trekvaarten, or tow-canals.

[…]

By 1700, an extensive network of trekschuit- and ferry services linked all of the important cities in the coastal provinces of the Netherlands. Travel by trekschuit was reliable, comfortable, and cheap. The speed was about 7 km/h, which was faster than walking, and more comfortable than by coach. Many foreigners praised the advantages of the system, leading to the introduction of canals, such as the Erie Canal, in the United States. The boats were pulled along by horse on a towpath (in Dutch called jaagpad, named after the jager (chaser) which accompanied the horse)”

Someone··on Overgrown, when plants invade your abandoned tabs
In a similar vein, Apple in the ¿’90s? toyed with the idea of making desktop icons show their age, and of making directories with lots of content bulkier and harder to drag around.

I don’t think that ever led to a real product.

Someone··on Oregon Police Are Charging a Local News Outlet $2.5M for Records About One Cop
And the post they replied to said “Having been on the other side, the delay may not be a deliberate strategy.”

That moves the needle back towards “may not be deliberate”.

Someone··on The result of the C++26 DIS ballot
Draft International Standard (https://committee.iso.org/sites/tc211/home/resolutions/isotc...)

This was the vote to promote the current proposal to draft standard.

Someone··on The Goose Programming Language
I think a human writer could easily have made that error, too.
Someone··on Today, we hacked what we'd set out to hack: the iPhone
> if apple parsed pdf with (js, swift, rust) none of this would be possible

Interpreters and compilers can have bugs. Bugs can cause memory safety issues.

Someone··on Blaise Pascal invented fixed route public transport (2024)
> Had this really not been done before? Apparently not on land. Ferries are an ancient idea, both for crossing water bodies and for traveling along them. They are fixed routes, of course, but that’s mostly because the shore is fixed.

Historically, not true for the “trekschuit” in 1632. For that, the shore didn’t exist before the route was envisioned. https://en.wikipedia.org/wiki/Trekschuit:

“The first trekschuit 'sailed' in 1632 between Amsterdam and Haarlem and could carry 30 passengers. The trekvaart or canal was dug in a straight line to facilitate an easy pulling process and to guarantee the shortest route”

Someone··on A robot I didn't expect to build
If the intended use is “1:1 replacing humans”, I don’t think it is surprising that a design that’s similar to a human is the superior design.
Someone··on Mini brain organoids ‘reading’ Braille key step towards biohybrid computing
Not if the organic tissue is faster or more energy efficient.
Someone··on A Markdown File Should Just Open
> Anyone who cares about Markdown has an IDE available anyway.

I think the point being made is that users who do not care about Markdown will receive Markdown files, and it should be trivial for them to open and view them.

Yes, the article also states “If I want to see the original Markdown syntax, I should be able to switch to that view just as easily”, which isn’t necessary for that use case, but I still think that’s a point the author makes.

Someone··on No more icons in every menu by default
> Exactly. There may have been a reason for the single menu bar back in 1984 when the Mac had a 9-inch screen. But it doesn't work very well on my 43-inch screen where the menu bar may be a few feet away from a small window in the lower right hand corner.

That isn’t obvious. With a mouse/trackpad with a good acceleration curve, chances are you can move faster to that menu at the top than to a menu a few cm away because you don’t have to decelerate when approaching the menu bar at the top of the screen.

Someone··on The compiler was supposed to end programming too
> Writing rules, or steps, unambiguously in a high level language and having those statements translated to lower level languages, that ultimately get executed by a machine, is what compilers do.

And it definitely is not what LLMs do, even if you pepper your rules with “NEVER, ever deviate from these rules”.

Someone··on Good type against all odds
It was invented for the teletype. https://en.wikipedia.org/wiki/Backslash:

“What may be the first documented reference to the character is a 1937 maintenance manual from the Teletype Corporation, which includes a photograph showing the keyboard of its Kleinschmidt keyboard perforator WPE-3 using the Wheatstone system. In a 1945 document, Teletype used the name "diagonal key" for the symbol, and gives it a (non-standard) Morse code of ._.._ . Neither document gives its usage”

> If a left handed person does it, its been invented beforehand

I disagree. A left-handed person writing a slash in mirror image doesn’t write a backslash; they write a slash using a different glyph.

Someone··on Good type against all odds
Firstly, in many cultures, people were forced to write with the right time up till the 1970s.p (https://en.wikipedia.org/wiki/Bias_against_left-handed_peopl...)

Also, when left-handed writing became accepted, there were special left handed pens (with a broader tip that you can push forward without it ‘biting’ into the paper)

Finally, how do you know nobody did that, and got harassed for writing incorrectly?

Left-handedness is somewhat associated with mirror writing (https://pmc.ncbi.nlm.nih.gov/articles/PMC2117809/:

“Particularly when produced spontaneously, mirror writing is a highly heterogeneous phenomenon: the mirroring may range from as small an item as a single reversed letter, through numerous reversed letters but not words, to thousands of pages of mirrored script; the place in the word in which a mirror letter occurs is variable, and numerals may or may not be reversed too”

Someone··on Is Cellebrite sitting on an iPhone radio 0day?
> So Apple quietly fixed a nasty vulnerability reachable over the air in iOS 26.5, yet they made no mention of it in the security bulletin

Alternatively, they changed the code but didn’t realize they fixed a vulnerability.

Someone··on Laptop Based on 6502 CPU
> this says 1024x600 and 256 colours

> I don't see where in the memory map there would even be enough space for a screen buffer that large to be located

1024 × 600 with 256 colours is 600 kB. Even in monochrome, it would be over 64 kB.

> but it looks like the LCD has to be bit banged by the CPU data bus directly?

Even at 20 Hz, that would involve writing over a ten million pixels per second, giving you about 1 CPU cycle per pixel ⇒ there’s no way to do that with this CPU.

Someone··on "Tame" boar and deer are instinctively adapting to the wolf in the Netherlands
> but their sudden reintroduction in the Netherlands feels ill thought out.

I don’t think it was a reintroduction, nor was it sudden.

AFAIK, they came back on their own accord, and their return was fairly slowly, after wolves returned to western Germany.

https://wolf.org/wow/europe/netherlands/:

“In a paper published in 2016, “The first proof of the recent presence of Wolves in the Netherlands,” authors wrote:

“In light of the expansion of wolves from the Polish border to the northwest of Germany and the sightings in Denmark, the appearance of the wolf in the Netherlands was no surprise to most experts. In March 2015, this expectation was fulfilled when, after generations without resident wolves, a single wolf wandered through the Dutch provinces of Drenthe and Groningen in broad daylight. From 7 to 10 March 2015, the Netherlands witnessed the comeback of an iconic species.”

Since 2019, the country has once again become home to its first pack of wolves with young pups after 150 years. Genetic sampling revealed the Netherlands wolves came from an Alpine population and Central European populations (i.e. Germany)“

Someone··on Anthropic assigned highest junk credit rating in June
No, but a trillion dollar company going to a ratings agency to get an assessment of its credit rating and not giving that ratings agency enough information to do that doesn’t inspire confidence in that trillion dollar company, either.

Why didn’t they give them the info? They either withheld it or don’t have it. Both make them look bad.

Someone··on Apple ML Research: Muse Spark Open with MLX on Mac Studio
They don’t lead with it. The title of the actual article is “Local and Distributed Large LLM Inference with MLX and RDMA on Mac Studio”.

The submitter changed it to “Apple ML Research: Muse Spark Open with MLX on Mac Studio”

Someone··on Apple ML Research: Muse Spark Open with MLX on Mac Studio
It’s not a press release and not about Meta’s technology.

The title (“Local and Distributed Large LLM Inference with MLX and RDMA on Mac Studio”) doesn’t even mention Muse.

It’s more like an advertorial for their tech.

Someone··on C++26 Contracts: Introduction to Preconditions and Postconditions
> If you wanted a c++26 preconditon for collatz tho, here it is.

  cpp bool collatz(unsigned long long n)
  {
    while (n != 1)
      n = n % 2 ? 3 * n + 1 : n / 2;
    return true;
  }
You’ll need to add code to detect cycles other than 1, 4, 2, 1, 4, 2,… to that. That can be done in constant space (https://en.wikipedia.org/wiki/Cycle_detection#Floyd’s_tortoi...)

Ideally, you also need a way to detect runs towards infinity. That is harder.

Otherwise, an optimising compiler can use the forward progress guarantee and optimize that to:

  cpp bool collatz(unsigned long long n)
  {
    return true;
  }
and then completely remove the precondition.
Someone··on Tesla Roadster
> But the base model will just be a regular Tesla.

A regular Tesla that sucks, you mean?

Even the base model has “active aerodynamics and a multi-mode suction system that maximizes downforce for next-level performance on and off the track.”

Someone··on C++26 Contracts: Introduction to Preconditions and Postconditions
https://en.wikipedia.org/wiki/Collatz_conjecture
Someone··on Your C is not standard C
https://en.cppreference.com/cpp/preprocessor/impl:

“ISO C language standard requires that C compilers support the following three pragmas, and some C++ compiler vendors support them, to varying degrees, in their C++ frontends:

  #pragma STDC FENV_ACCESS arg      (1)
  #pragma STDC FP_CONTRACT arg      (2)
  #pragma STDC CX_LIMITED_RANGE arg (3)
where arg is either ON, OFF, or DEFAULT.”

⇒ it seems C compilers must support this (but C++ compilers need not)

Someone··on Apple Keynote now showing ads in its UI
Objectively, this isn’t much different from an app offering in-app purchases.

Subjectively, however it feels significantly different to me.

Reasons why that’s the case that I can think of are:

- it shows the offer even when users aren’t searching for the offered product?

- the product that is offered doesn’t signal “in-app purchase”?

- it doesn’t feel like Apple to do this in this way.

Page 1 of 34Next →