FoxQuirk 🦊 @quirk@computerfairi.es

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/

“ah, no no, that factoid about Araragi-senpai is only established in a deuterocanonical work, I'm a Protestant”

this may as well be the Bible they're gonna be unearthing new Monogatari stories for centuries to come

reading the Japanese Wikipedia article there are how many Monogatari series short stories?!

Today, #Coreboot met #FreeBSD.

https://cgit.freebsd.org/src/commit/?id=5f74217c05a99f38a31a6e4950220964595d4ac8

When I started writing FreeBSD drivers, a friend told me:

So you’re just copying Linux drivers and rewriting them for FreeBSD ? Sounds like script work.

I explained that it doesnt work like that. First you understand the hardware. Sometimes you have to reverse engineer it. Then you test it. Only after that do you submit a driver.

He replied:

Fine. Then write a driver that doesn’t exist in any operating system.

That turned into a 500 MAD bet. (MAD is Morocco’s currency, not a measure of my sanity.)

The challenge is harder than it sounds. Almost every piece of hardware already has a Windows driver, a MacOS driver, a Linux driver, or follows a standard interface.

You dont invent hardware. You find a missing need.

So I wrote a driver for Coreboot.

Normally, the kernel log starts when the kernel boots. Everything that happened before that is a mystery. You can make educated guesses, but thats all they are.

With this driver, FreeBSD can read the Coreboot log. You get to see what happened from the very first moment the machine powered on.

That is exactly how I tracked down systems where RAM training was taking far too long because of defective memory chips.

None of this would have been possible without the amazing work of the Coreboot team.

As far as I know, FreeBSD is now the first operating system with this driver.

DragonFlyBSD is next.

Thanks to doordash building drones it will be the first time in history you can hunt a flying robot and collect food from the remains.

This behavior will be encouraged until morale improves.

I really like Procreate's Statement on AI. https://procreate.com/ai

#NoAI #AIPlague

left the house with the orb running and came back to this

it's actually way, way worse than I implied, and this isn't any kind of joke

You can get SIX computers for the price of a nice sub sandwich delivered to your door

going back in time and telling baby!Alice that one day, you'll be able to go online and order a computer 8 times faster than her packard bell, with dual cores, and it'll arrive within 24 hours.

and she'll also be able to do the same for a sandwich, and the sandwich will cost more

I dunno why there are so many OLED/LCD modules for the pi pico that use a nice header that cleanly fits over all the pins

so it's great if you want to easily connect a display, terrible if you need to connect it to LITERALLY ANYTHING ELSE

the pico has like 30 GPIO pins! your OLED is NOT using all 30 of them!

I just went and installed it on Win98 since Win3.1 was crashing every time

added basic enemy attacks to You Have Died (And Been Reincarnated As A Fox Girl), a game about being reincarnated as a fox girl in a dungeon town where everyone else is also isekaid girls and gay shenanigans and dungeon diving ensue

Them: nature made MALE and FEMALE and you can’t change it

Nature:

RE: https://beige.party/@rooster/117000952913461604

we really got genderfluid avocados before gta 6

the movie “O Brother, Where Art Thou?” is actually about me trying to find the IP address for my wife’s printer

Would you prefer a job where:

a) Work meetings are never recorded and AI notetakers are never used, but you have to take notes manually occasionally.

b) Or a job where meetings are regularly recorded and are using AI notetakers, but you never have to take notes.

@Em0nM4stodon Needs to be filed under "Why abled people should care when disabled people bring up issues"...

At least at the University of California, for disabled people at UC (whether students, staff, or faculty), there used to be human notetakers for those who had that access need. It was a good work/study job for abled students to be a notetaker.

But since disabled people are always seen as a risk and cost "to be managed", the moment that abled decisionmakers could fob it off to Otter .ai, they did. This compromised privacy of disabled people. But people didn't care when it was mostly happening to disabled people...

Of course, as soon as the tech was available to have these AI notetakers in online meetings, abled folks began to notice.

The cruel irony is that AI corps love using "accessibility" as cover for their work. But if abled decisionmakers cared about accessibility, everything would already be accessible as possible. It's not about accessibility.