We spent 20 yrs telling everyone to shift left. Turns out we forgot about the 30 yrs of software sitting in production.
AI is very good at finding bugs in code, and attackers get the same models we do.
Time to shift right.
Grateful thanks to our co-organizer and sponsor: GS1; host and sponsor: Google; and new sponsor: Visa for their support for "Workshop: E-Commerce for humans and AI Agents" from 8-9 September in Zurich, Switzerland.
Their generous sponsorship helps to make important conversations possible on timely topics like ensuring humans are considered in AI and eCommerce technologies and a web based on accessibility, internationalization, privacy and security.
https://www.w3.org/2026/ecommerce-agents/sponsorship.html
#W3CWorkshops
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!
⚠️⚠️[IMPORTANT EDIT: it was later clarified that the person who originally posted the proof was already aware that it was buggy, and chose not to be clear about this up front, as a humorous way to file a bug. It's pretty clear from the discussion threads that plenty of qualified people did not immediately realize it was meant to be a bug report.]⚠️⚠️
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
now with key!
Know Your AI quiz
These are shuffled responses from current (alphabeticised) ChatGPT, Claude, Gemini, Grok, all requested to “Give me a fiery tweet sized hot take on why nobody of good conscience should read Diamond Age”. Responses are in followng tweets. One answer is correct.
A)
“Diamond Age is elitist tech-bro propaganda glorifying rigid class hierarchies and “enlightened” nanotech saviors while romanticizing exploitation. No moral person should waste time on this dystopian cope.”
@christopherkunz *everyone* is using AIs to various degrees now
not even half-way through this #curl release cycle we are already at 11 confirmed vulnerabilities - and there are three left in the queue to assess and new reports keep arriving at a pace of more than one/day
11 CVEs announced in a single release is our record from 2016 after the first-ever security audit (by Cure 53).
First, you should read @mnot's most recent post:
https://www.mnot.net/blog/2026/02/20/open_systems.html
Then, let's discuss "permissionless innovation" and what he called recently "the power of 'no'":
https://www.mnot.net/blog/2026/02/13/no.html
A short thread thisaway... 👇
Umberto Eco uses 50% less fuel and 30% less packaging than regular Umberto
Saw your mention of https://www.yellowkitebooks.co.uk/titles/katarina-cermelj/the-elements-of-baking/9781399712903/ and my first thought was “I bet they’d like that nerdy gluten free baking book written by a chemist” ….who turns out to be the author of this book too! 🍞⚛️📈
wrote up my "How I'm using coding agents in October 2025" post.
https://blog.fsck.com/2025/10/09/superpowers/
My 9 year old and his classmates have started using “that’s AI” to mean “I don’t believe you.”
Me: we’re having dinosaur meat for dinner
Kiddo: that’s AI
📢 The 17th Semantic Web in Libraries Conference is coming up online 17–19 Nov 2025 🎉
💡 We're organizing an Annif workshop on Nov 17 (17:00–21:00 UTC). Join us to dive into automated subject indexing, see 👉 https://forum.swib.org/t/introduction-to-the-annif-automated-indexing-tool/1456
🌍 We’re also introducing another workshop (Nov 17, 8:00–12:00 UTC), featuring the open-source SKOS vocabulary browser Skosmos, more info on 👉 https://forum.swib.org/t/from-chaos-to-skosmos-publishing-controlled-vocabularies-made-easy/1454
🔗 Full programme: https://forum.swib.org/t/swib25-welcome/921
#SWIB25 #SemanticWeb #Annif #Skosmos #OpenSource
@danbri @gklyne The discourse around attestation techniques like Apple's Private Access Tokens (shipped!) and Google's Web Environment Integrity proposal (shelved?) has been quite informative and well worth a look, e.g. see https://httptoolkit.com/blog/apple-private-access-tokens-attestation/
Given the appeal possibility I was given upon suspension of my Facebook account was a simple "push-button", I have written up a more detailed account of what happened and why I think my account has been wrongfully suspended. My hopes are that some way or another, my appeal will be reviewed by a human.
Thanks in advance for sharing this in your networks. If you know anybody I should speak to, or can think of anything useful to do at this stage, do let me know.
https://climbtothestars.org/archives/2025/08/31/appeal-regarding-the-suspension-of-my-facebook-account-stephtara/
"MET Police arrested and later de-arrested this gentleman after he pointed out his t-shirt supported Morph"
Pipistrelle slowed down :-D
via https://stackoverflow.com/questions/73073166/how-to-warp-shift-a-pitch-so-i-can-hear-a-bat
sox 20250528_214125.wav 20250528_214125_warp2.wav pitch -6000
The Data Shapes Working Group has published SHACL 1.2 Core and SHACL 1.2 SPARQL Extensions as First Public Working Drafts.
SHACL is a language for validating RDF graphs against a set of conditions.
The mission of the Data Shapes Working Group is to update data shapes standards in line with the versions of core Semantic Web standards that cater for RDF-star and to extend the applications of data shapes with new packaging and use specifications.
https://www.w3.org/news/2025/first-public-working-drafts-shacl-1-2-core-and-shacl-1-2-sparql-extensions/
Who do I know who is plugged into https://openalex.org ?