FoxQuirk 🦊 @quirk@computerfairi.es

#capitalism #sustainability

why debug a bunch of bitfiddly C code when you can just waste 5kb of code space?

I was dreading have to port and test some finicky code from python to C but then I realized that for my uses, there's only 201 possible inputs to the function, each of which results in like 24 bytes of output

I can just make my python code enumerate them all, stick them in an array, and now the C code never needs to generate shit

wait I just realized I could avoid having to be smart by just being stupid harder

My mom has been running a community art & poetry project using the fence around her home for the last 15+ years, which she calls The Poetry Fence. She takes it very seriously and uses it as a base for all sorts of poetry outreach in her neighborhood. She's recently written a book about her experience with this project which she's trying to get published by a small press.

And in her mid-70s, she's just created her first ever website. It'd mean a lot to her if you take a look! https://www.poetryfencecommunity.com/

She doesn't know I'm posting this, but if she did she'd probably want me to add that science is real, no person is illegal, trans rights are human rights, and banned books are worth reading. And most of all, that poetry is for everyone.

Boosts on her behalf appreciated.

#poetry #community #SmallPress #publishing

#AI

Alright fedi, can I have a recommendation for an email provider which:
- is not based in any country on earth, or at the very least, no UN-recognised nation
- has a no-log policy only in the summer, as I have a fireplace in my house so I gotta be burning those logs when it gets cold
- supports end-to-end encrypted lucid dreaming
- is completely vegan and ideally fairtrade, but rainforest alliance is also fine
- supports using other people's domains, I like those more than mine
- allows for text formatting in green, and also, ideally, red. I love my friends Green and Red.
- has diplomatic treaties with other mail providers

On Google shutting down AlphaFold.

it's a common misconception that the Windows GDI stands for “Graphics Device Interface”. it actually stands for God Damn It, because its arcanities will make you want to kill yourself

oh god rgba(255, 0, 0, 255) gets alpha-blended on Windows XP as rgb(254, 0, 0)

I need to add an epsilon 😭

A tagged subway car will always look better than one fresh from the factory. Why shouldn’t people in the city beautify their own trains? Why do we let them fill up with advertising instead?

If you're in Australia, Trans Justice is running a survey about access to and experiences with gender confirming health care, to provide data in support of their work pushing for better access. Seems designed to include DIY experiences, and those who want access but have yet to get any care. Open to all trans and gender diverse people in Australia
https://transjustice.org.au/survey/
#Trans #Australia #TransgenderHealthcare

girls only want one thing and it’s for mikrotik’s dhcpv6 to say “Status: bound”

got the bit-endianness of a bitmap format wrong again award

Yes I did transcribe alt text for this. My eyes hurt now.

Okay, we have a new contender for Most AI Thing to Ever Happen

1) July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem prover. (The AI use is not disclosed on the github page) https://github.com/xrchz/CollatzLean

2) July 26th: several serious bugs are posted in the theorem provers, that in principle could allow a false statement to be "proven" true. They're serious, yes, but no need for panic, because you're not going to blunder into accidentally exploiting the bugs while writing a proof, probably.
https://github.com/leanprover/lean-kernel-arena/pull/81

3) July 28th: someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug https://github.com/leanprover/lean4/issues/14576

4) The "proof" turns out to be exploiting multiple similar but distinct bugs to pass different solver variants!

5) the human who posted the proof acknowledges the AI use and claims they did not knowingly point it towards the bugs it exploited. https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613135216

Note that the proof was posted shortly before the related bug reports were posted. It is an open question if the AI found people discussing the bugs shortly before they were formally posted and "decided" to exploit them, if the AI "knew about it" as a learned strategy from the training stage (putting every single "proof" it's ever made and ever will make into profound doubt), or if it's recently been repeatedly blundering into it by sheer stupidity and that's how people noticed the bug at about the same time.

Theorem provers aren't magic, and have bugs just like all other programs. They are tools to help us double-check our reasoning. When you skip the reasoning and ask an AI to "prove" something for you that's over your head, you're entering an adversarial pact with the monkey-pawed Devil of Customer Satisfaction.

my initial source for investigating this myself: https://lipn.info/@mevenlennonbertrand/116997927457012577

Ever wished you could have multiple independent mouse cursors on your Linux machine? No?

Anyway, turns out Wayland supports that pretty well! Let me tell you what I learned:

https://blinry.org/multi-seat-wayland/