News for hackers. Stuff that matters.

penteract

Re:Classification of Finite Simple Groups Formalized in Lean on Tuesday October 27, 2026 @05:43PM (#50266269)
Producing a formalized proof from a non-formalized proof in a paper or book should not be considered a violation of copyright.
Re:A Strongly Aperiodic Monotile in Three Dimensions on Wednesday October 14, 2026 @11:48AM (#50089566)
Yeah, the seven cubes shape tiles R^3 by itself following the aperiodic tiling, but it also tiles R^3 in other ways, some of which are periodic. The bumps prevent any of the periodic tilings. See [1] for a better explanation with a picture of the shape as a rep-tile, and [2] for insight into how a rep-tile becomes an aperiodic tiling.

[1] https://arxiv.org/abs/2609.24779

[2] https://en.wikipedia.org/wiki/Rep-tile#Examples

Re:A Strongly Aperiodic Monotile in Three Dimensions on Wednesday October 14, 2026 @04:22AM (#50084191)
I suspect they've spent much longer looking at 2d shapes than 3d ones (because they're easier to imagine and reason about, and there are fewer variations in how "aperiodic monotile" can be defined in 2d).

Also, the tricky bit for this kind of shape (similarly to Penrose's tiles) isn't finding the shape, but finding the aperiodic tiling and adding gadgets that rule out any periodic tilings (and proving this). The actual aperiodic monotile shown looks like it has 201 faces (although that could trivially be reduced by quite a bit).

Re:Worlds More Habitable Than Earth? They're Out There on Tuesday October 13, 2026 @03:57PM (#50077746)
For the sake of pedantry, there are things in the observable universe which are increasing in distance from us by more than 1 light year per year. This means it's impossible to reach them unless the universe's rate of expansion changes. I think the Hubble volume is the region theoretically reachable; limiting acceleration to 1g would limit you to a slightly smaller region (only a tiny bit smaller, I think).

https://en.wikipedia.org/wiki/Hubble_volume

I read pretty much the same thing. First * is 'discontinuous', second might be 'turn'. I'm tempted to read 'continuous' where you have 'containing'.
a) Self driving was far from completely solved before LLMs.

b) Text generation essentially means passing the Turing test, which for a long time was the bar for general intelligence. Locomotion does not necessarily require general intelligence.

Re:Learn Programming with OCaml on Sunday September 06, 2026 @11:04AM (#49587169)
> I believe that an ML should be the First Language for Computer Scientists.

I'm not sure how much influence a First Language has - the biggest impact might be whether someone decides to continue learning to program. I'd also worry that we might lose something if all computer scientists are too similar. There are lisp believers, and there are those who swear by C; and I think the field of CS would be less rich if either were missing. Given that, it's a good thing that there are a variety of languages taught as first languages, and I'd like to see the variety widen (I don't know of any CS degree which begins by teaching Forth).

> Some languages are less permissive, and have a culture of searching harder for corner cases and dealing with them than others, that is true. I would expect to find less cases like this in Rust, but more cases like this in Python.

My expectation is that when I think I've found a bug in the programming language implementation I'm using, it's actually me that's mistaken (or at least that language lawyers consider me to be mistaken). Hearing about someone who has encountered multiple bugs (in regular use, rather than running a fuzzer or being directly involved in implementing the language) makes me very wary.

There has been an instance of a Governor General dismissing a Prime minister.

https://en.wikipedia.org/wiki/1975_Australian_constitutional...

Re:Fable and the End of the Free Lunch on Monday August 24, 2026 @07:18AM (#49418148)
To me it sounds like you're repeating what gp said about the lack of online learning. Do you think that's insurmountble?

Getting confused about timezones does not place LLMs behind that many humans. (But doing so repeatedly does highlight the lack of online learning).

Re:Death to px, long live ch on Monday August 24, 2026 @06:44AM (#49417875)
It never says 0.04 degrees, just 0.04mm (corresponding to about 0.015 degrees at the stated 15cm distance).
Re:A joke domain purchase turned in geopolitical warfare on Wednesday August 19, 2026 @07:14PM (#49368405)
> like they found for Russia tracking launch sites in Ukraine

My understanding of that section was that Ukraine were using it to find launch sites in occupied parts of Ukraine - they go on to describe how they helped someone who had been doing the tracking:

[From article]

> We emailed back and forth and provided documentation on how to run the predictor locally.

Edit: my recollection of which parts of Ukraine are occcupied was wrong, leaving me rather confused about who they thought they were helping.

Re:Incident with Github.com on Monday August 17, 2026 @08:55PM (#49339793)
Please could you link to the study if you can find it. The definition of "better" seems quite critical here, as well as whether it's specific to code hosting websites. A messaging platform is pretty useless if I'm the only user, but Github would still be useful to me without anyone else having an account.
Re:Rust SIMD on the GPU on Tuesday August 11, 2026 @05:39AM (#49255493)
>> GPUs aren't really SIMD, they're SIMT (single instruction multiple thread)

> False. If they were threads they'd have their own PC. They do not - only the warp has a PC.

They are using the term SIMT as it is normally used[1]. The "single instruction" part means that there is only one PC shared across multiple 'threads'.

[1] https://en.wikipedia.org/wiki/Single_instruction,_multiple_t...

Re:So you want to use plants to reduce CO₂ on Thursday July 30, 2026 @09:20PM (#49117984)
Did you consider the alternative calculation of how many plants you need to grow to feed yourself? A few thousand potatoes growing simultaneously might do it.

That would overestimate the number you need to remove excess exhaled CO2, since you could throw out the parts you can't eat rather than letting them decay and release CO2 indoors.

Re:We have proof automation now on Monday July 27, 2026 @11:59AM (#49071476)
> dependent types and total functions do not scale.

I'm not convinced that this is much more true than the claim "correct code doesn't scale". If you add to your code in a way depends on a new property for correctness, and the code was not previously written with awareness that the new property was necessary, then you need to check through the rest of your code and make sure that the property is maintained. Formally verifying things is painful because it actually makes you check this.

Instead, we live in a world where we use software that is not completely correct. Browsers have remote code execution vulnerabilities because people who make browsers decided it's more important that javascript can run quickly, and that new standards get implemented, than that we avoid such vulnerabilities at all costs.

Re:Jaron Lanier: there is no AI (2023) on Monday July 20, 2026 @06:04PM (#48985451)
If you had access to a bunch identical copies of me that couldn't communicate with each other, you'd be able to find many questions I would give stupid answers to. I suspect I'd come out of it looking worse than an LLM.
Re:Why do AI company logos look like buttholes? on Saturday July 18, 2026 @08:02AM (#48957288)
This brought to my attention the following claim by OpenAI, regarding a logo which does not have any right angles:

> right angles introduce the precision and structure that technology demands

https://openai.com/brand/#:~:text=right%20angles

Re:Australia is offering free daytime electricity on Tuesday July 14, 2026 @07:40AM (#48905181)
To check I understand you: the smaller tank with heatpump would consume less energy outside the time window in which energy is free than the large tank with resistive heating, but has a higher capital cost which would outweigh the amount saved on energy?

If that's right, it's not obvious to me that building a suitably sized solar panel is environmentally worse than building a heat pump.

Re:The Graph That Should Be Front-Page News on Monday July 13, 2026 @08:33AM (#48891738)
Based on https://climatereanalyzer.org/clim/sst_daily/?dm_id=nino3.4, 1988 is the year from the dataset with the lowest temperature throughout June and July.
There are those who make strong arguments for the opposite.

Once you have paid him the Danegeld, you never get rid of the Dane.

The number €115 is in the second chart as the per capita German expenditure on rail infrastructure in 2023. I don't see €477, but it's pretty close to the €480 figure for Switzerland in 2024. My guess is they saw an old version of the page when the first chart had numbers for 2023 and have kept using it without noticing the update.
It's saying that 40% of the tons of cargo loaded onto ships is fossil fuels, but this makes up about 50% of ton-miles, because fossil fuels travel further on average than other cargo. Not the easiest headline to correctly parse.
Re:Alice is impatient on Sunday June 21, 2026 @06:42AM (#48617611)
This is the same calculation behind the observation "you spend much longer in front of red traffic lights than green ones".

It's an interesting observation, but it's playing games with the meaning of "mean latency" and I'm not sure this is a very helpful way to look at requests to a web service - slightly slowing the fastest responses to requests would improve your time-weighted mean latency.

It's a better metric for looking at outages - instantaneous outages don't affect anyone, and time-weighting correctly discards them. On the other hand, average outage length is a very suspect and gameable metric unless accompanied by uptime %.

Re:What every coder should know about Gamma Correction on Tuesday June 16, 2026 @08:26PM (#48564214)
> What you want is 40% black onto white to have a similar difference in intensity as 40% white onto black, otherwise your darkmode font will look significantly different at the same intensity as your lightmode font. This is why it doesn't make sense to do it in a linear colourspace

Thanks for putting this clearly. I had not given this argument enough thought and respect previously. Would you agree if I said this is about maximizing the amount of useful information given to the reader (even if it deviates from approximating a printed page) and a perceptual colour space is the way to measure that information?

I should mention that I can find plenty of resources that suggest you should use a different font for dark-on-light vs light-on-dark (although I'm aware I'm not a good judge of the quality of said resources). This is not necessarily opposed to your point, since your reasoning can be extended to conclude that identically shaped printed text subject to blurring in linear colour space would be perceived differently depending on whether it's light-on-dark or dark-on-light (including when it's naturally blurred due to imperfect eyesight).

> Note that the Wikipedia article is wrong, given that photoshop uses a nontrivial gamma exponent

If we set text rendering aside, and consider something like games which prioritize photorealism rather than legibility, would you agree that linear colour space is the sensible one to do antialiasing in? This is for essentially the same reason you should do image resizing in linear color space, for which Wikipedia's citation [6] provides a convincing demonstration.

[6] https://www.ericbrasseur.org/gamma.html?i=1

Re:What every coder should know about Gamma Correction on Tuesday June 16, 2026 @10:27AM (#48555860)
> There's no physical underlying lighting process, so it doesn't make sense to use physical light units.

I disagree with you here. Text rendering specifically is incredibly complicated, but for antialiasing in other contexts, the problem can be seen as trying to approximate what would be seen if the display had higher resolution and the viewer has blurry eyesight. In this model, a linear color space makes sense - if 60% of the pixels within a region on a higher dpi display would be lit, then that is best approximated* by a single pixel emitting the same number of photons as those pixels would (which is 60% as many photons as there should be in the situation where all pixels on the higher dpi display would be lit).

See https://en.wikipedia.org/wiki/Spatial_anti-aliasing#Anti-ali... .

*there are better filters if you're looking at more than one pixel at once

> Using perceptual blending, the antialiasing will be exactly the same efficacy in both cases. Using blending in linear space, these two test cases will look very different and render incorrectly!

Whatever color space you do your blending in, 40% black onto white should look the same as 60% white onto black.

Re:An O(x)Caml book that runs on Monday June 15, 2026 @08:01PM (#48548803)
Yes for me (although difficulty varies depending on what you're trying to install). I would have started programming 2 years earlier than I actually did if my first attempt to install tools to run a programming language had worked.

You have to precisely follow a sequence of instructions without the experience to understand their purpose, or any idea of to fix things if you make a mistake.

Web technology is an exception to this. People already have a web browser, and ignoring mobile devices, browsers come with a js REPL.

Re:Anthropic's Safety Superpower on Monday June 15, 2026 @10:21AM (#48541730)
The article makes a coherent argument:

a) Anthropic believe that AI is an extinction level risk and that they are the only leading AI lab which takes safety seriously. In combination this puts them in the position of believing that they are the only ones who can save the world, which is reasonable to call a god complex.

b) Anthropic are engaging in actions which aquire and consolidate power in the form of control over powerful AI.

c) "The history of brilliant people convinced they know what humanity needs is a sordid one, precisely because they have convinced themselves that their intentions are good, justifying actions that very much are not."

I'm describing claims from the article and would not word them so strongly myself. But this explicitly does not assume evil intent.

Note that the US military is almost the only customer that Fable and Mythos could safely be sold to while complying with this directive.
I'm a bit more interested in what it teaches about the hyperbolic plane than I am in it's effectiveness as a note taking app (although the way it supports an exponentially growing tree does seem appropriate for depicting knowledge - I'd be interested to see something like a force directed graph of Wikipedia plotted on the hyperbolic plane).

The points and arrows do move and change shape appropriately while panning, but the images and text do not. It might be possible to use feDisplacementMap (an SVG filter effect) cleverly to get the deformations right. This would probably make performance worse, and I'm not sure how readable the text would be, but it would mean that things wouldn't start overlapping each other while panning.

Older »