@wilbowma it's the same reader system used by multiple other publishers. I'm sure it's analytics.

@wilbowma it just keeps getting worse

It's taken many years, but I'm finally in a situation where I have no choice but to learn SSReflect. And... I kinda like it? It's totally inscrutable, to the point where it kind of makes the critics' point about unreadable computer proofs. But it's so damn efficient for *writing* proofs. Has anyone ever tried writing a tool to translate SSReflect proofs into standard Ltac proofs?

This is gonna sound like a call out post, and... No, it really isn't. I'm not calling out anyone in particular. I've just seen it one too many times. The straw, the camel's back, yadiyada.

My cis dudes. I love you. I really do. But I'm tired of you going under women's post expressing their grievances about men, to explain how ashamed you are of other men. It's... It's tiring. Like, it's really fucking tiring. Because you don't realize that every time we make such a post there is at least one or two of you. Every time.

We don't care about you being not like the other guys. Yes, sure, are one of the good ones, whatever. Good boy and all that. But when you do this, not only do you not contribute anything to the discussion, you're actually adding to the problem. It's adding emotional labour to the women trying to explain themselves when really you should just stay quiet and listen.

Give a like. Boost the post, even. But you don't need to say anything, not to us. Call out other men in the responses that are probably trying to argue and ending up exactly proving her point. Do better, instead of saying that you already are.

#fedi #men #women

They can’t cancel the midterms.
So they’ll cancel access.

The SAVE Act is the latest attempt to bury women’s votes under bureaucracy—ID rules that don’t match married names, proof many don’t have, and hurdles that hit women, the elderly, and caregivers hardest—then call it “election integrity.”

Making it “harder to vote” is just voter suppression in a suit. #election

https://www.theguardian.com/commentisfree/2026/jan/31/save-act-voting-arwa-mahdawi #press

@paulmelis frankly the information security and research integrity implications of this irresponsible piece by a tenured professor warrant a stronger response than 'keep a backup'. Dumping coauthored drafts, grant proposals, email correspondence, and student data (!) in a commercial ChatGPT Plus account, while knowingly giving OpenAI consent to train on all of it for >2 years, amounts to violating every professional guideline and breaching the trust of everyone you work with

The program for the Oregon Programming Languages Summer School 2026 looks exciting: https://www.cs.uoregon.edu/research/summerschool/summer26/

Come or send your students!

Topic for debate: the ICORE rankings from Australia have done more to harm research than to improve it. They foster a short-term, zero sum leaderboard approach to science, require enormous amounts of time to participate, and in the end confirm what the community already knows.

RE: https://mastodon.laurenweinstein.org/@lauren/115963873612884664

Reminder that in the UK in 1900, before mass vaccination for childhood diseases began, 20% of all babies died before their fifth birthday (from diseases we currently vaccinate them against).

RFK jr's appointee wants to kill roughly 20% of all newborn Americans "to improve the breed" or something.

(Not including those paralysed for life by polio.)

We knew this was coming, but now the clock is running. From Privacy International:

"Yesterday the Trump Administration announced a proposed change in policy for travellers to the U.S. It applies to the powers of data collection by the Customs and Border Police (CBP)."

"If the proposed changes are adopted after the 60-day consultation, then millions of travellers to the U.S. will be forced to use a U.S. government mobile phone app, submit their social media from the last five years and email addresses used in the last ten years, including of family members. They’re also proposing the collection of DNA."

PI linked to and summarized a Federal Register entry describing the proposed requirements:

-All visitors must submit ‘their social media from the last 5 years’

-ESTA (Electronic System for Travel Authorization) applications will include ‘high value data fields’, ‘when feasible’
‘telephone numbers used in the last five years’
-‘email addresses used in the last ten years’
-‘family number telephone numbers (sic) used in the last five years’
-biometrics – face, fingerprint, DNA, and iris
-business telephone numbers used in the last five years
-business email addresses used in the last ten years.

https://www.privacyinternational.org/news-analysis/5713/trump-administration-wants-your-dna-and-social-media

The Federal Register entry says comments are encouraged and
must be submitted (no later than February 9, 2026) to be assured of consideration.

Federal Register entry: https://www.govinfo.gov/content/pkg/FR-2025-12-10/pdf/2025-22461.pdf

Of course

Seen this around without alt text, so I yoinked it to post it myself.

Edit: Based on the earliest mention known and reminded to me (thank you!):
https://mastodon.social/@mhoye/115742732861618099

Why do Danish airports play so much American country music? It's all I've heard for the last hour at AAR

@ricci a wrapper around the real LinkedIn front page where everything is upside down except for a conspicuous link in the corner for reporting problems with the "new" website (which reports the problem to the actual LinkedIn)

@ricci 6 hours is not long enough to cover the required apologies.

Copenhagen airport is really nice. But I should have tried harder to avoid a 6 hour layover.

Does anyone have links to ceramic artists on the fediverse who make and sell food-safe pottery items, like mugs and bowls, and that could be sent to a US address?

#Ceramics #Pottery

@flippac @pozorvlak most 64 bit hardware until the last few years is effectively limited to 48 bit addresses because nobody built systems with that much RAM. Maybe related to that?

@krismicinski @chrisamaphone @jonmsterling the Lean community half-embraces, or at least actively tolerates it. Many Lean related events are now sponsored by AI companies. But core Lean, mathlib, and cslib all regularly reject AI-generated pull requests, so it's not in the main libraries.

Bad proof assistant usage predates LLM slop though. I reviewed a number of papers pre-2022 that had reasonable sounding results but did weird stuff in Rocq formations like try to encode universal claims as individual instances of some inductive data type. So they'd claim they proved some universal but they actually just proved there existed one case where it worked, without using induction on something that clearly needed it. I saw that one a number of times. And of course I've seen more subtle misformalizations, too.

@joomy workshop proposals were just due last weekend, so nobody officially knows yet