Wasm 3.0 Completed https://lobste.rs/s/bqiqjm #release #wasm
https://webassembly.org/news/2025-09-17-wasm-3.0/

Ask HN: Is anyone else sick of AI splattered code

Discussion: https://news.ycombinator.com/item?id=45278819

Woodland sunflowers still going strong

X, Facebook, Threads, Instagram, and now TikTok – not to mention much of legacy media – are aligned with the despotic regime in the US.

It's never been more important to have a mindful media diet.

We, who are already on fedi, must help our friends and family migrate to better platforms and news outlets.

A structured representation of tactics for machine-assisted theorem proving. ~ Jade Master, Vincent Wang-Maścianica, Zanzi Mihejevs, Bruno Gavranović, Andre Videla, Dylan Braithwaite. https://www.renaissancephilanthropy.org/a-structured-representation-of-tactics-for-machine-assisted-theorem-proving #AI #Math #ITP #LeanProver

なんか 03:00 になっていた。

What makes Bluesky different: it’s open source, so anyone can contribute to building the experience they want. And even if you build a whole new app, the protocol means you can migrate with your data, identity, and relationships intact.

RE: https://bsky.app/profile/did:plc:bvdrfwiamgi5leqs63q2duro/post/3lytek7zud72s

因買嘢同店員嗲咗幾句，佢問我邊度嚟，我就話香港。跟住佢問我：好多香港人都唔prefer被叫做Chinese，可唔可以話我知點解？

跟住我就棟咗喺舖頭同佢極速用咗十分鐘快速地講咗來龍去脈，歷史背景呀以前香港係佢大英祖國殖民地（佢完全唔知😂）呀英國點交香港俾大陸呀矛盾呀衝突呀，佢一邊聽一邊點頭然後又問下問題我又答下。

佢：咁即係你地淨係用嘅語言文字都唔同？
我：唔同呀。
佢：哇，諗下都覺得會好痛苦。
笑嘆咗口氣，我話：係囉，估都估到會幾痛苦。

佢問我仲會喺倫敦留幾日，我話好快走啦，佢話係咪返香港，我話唔係呀返東京。

佢問：點解搬咗去東京嘅？
好多情緒湧上心頭，只好講句：原因好複雜。

踏出舖頭等巴士，企喺現代與西式建築並立嘅街頭，有瞬間錯覺自己喺中環等車返屋企。

店員最後條問題言猶在耳。
係囉，點解呢？我都想知點解。

Hot take: free and open source is fundamentally incompatible with strong security *guarantees*, because FOSS is incompatible with strong guarantees about anything. It says so right there on the tin: "without warranty of any kind, either expressed or implied". We guarantee nothing by default, you get the code, the project, everything, as-is, where-is, how-is.

Of course companies find this inconvenient, especially with the EU CRA looming, but that's not FOSS's problem. That's a you problem.

Bridging proof and computation (For a verified Lean–Macaulay2 interface). ~ Matthew Ballard, Anton Leykin, Damiano Testa, Michael Stillman. https://www.renaissancephilanthropy.org/bridging-proof-and-computation-a-verified-leanmacaulay2-interface #AI #Math #ITP #LeanProver #CAS #Macaulay2

[Parametric type design in the era of variable and color fonts] by Santhosh Thottingal (@sthottingalSanthosh Thottingal), 2025
https://arxiv.org/pdf/2502.07386 #typograhy #fonts #metafont #parametric

Constraining LLMs for theorem proving (A neurosymbolic approach to guaranteed autoformalization). ~ Eleonora Giunchiglia, Sam Adam-Day, Joshua Ong, Mihaela Cătălina Stoian, Luca Andolfi. https://www.renaissancephilanthropy.org/constraining-llms-for-theorem-proving-a-neurosymbolic-approach-to-guaranteed-autoformalization #AI #Math #LLMs #ITP #LeanProver #Autoformalization

enshittification, die:
Qualifizierte und teure EntwicklerInnen durch "vibe coder" ersetzen und dann zusätzlich billige "Vibe Coding Cleanup Specialists" einstellen.
#Lohndumping #enshittification

Mesa is working to update our contributor guide. Can you guess why?

Did you guess AI?

Because if you did, you'd be right. I don't want to put anyone on blast here so please don't go digging to find the motivating MR and harass the contributor or anything like that.

But the situation was exactly what you might think. Someone ran ChatGPT on the code and asked it for suggestions on making it more performant. They applied a bunch of the changes against their local branch, tested it, and found that it gave maybe a 0.5-1.0% perf boost in some titles.

That's totally fine. I don't care what tools you use to find a bottleneck. I'll happily take more FPS, no matter who found the issue or how. If some AI assistant helps you find things no one else has found and lets us make drivers faster, great!

But that's not what happened.

What happened next is that they then tried to make it the Mesa project maintainers' job to sort through the shit ChatGPT spit out and decide what's useful and what's not and why the changes helped and whether or not they were correct. The contributor had no no idea and, more importantly, they had no desire to actually learn about the Mesa code-base or the hardware in question. They just wanted to run ChatGPT and send its suggestions towards upstream.

This is not useful. This is not contributing. It's just burning maintainer time sorting through AI hallucinations. We have enough mediocre code to review that comes from actual humans who are actually trying to learn about Mesa and help out. We don't need to add AI shit to the merge request pile. If you don't understand the patch well enough to be able to describe what it does and why it makes things faster, don't submit it.

So now we're making it really clear: If you submit the merge request, you're responsible for the code change as if you typed it yourself. You don't get to claim ignorance and "because the AI said so". It's your responsibility to do due diligence to make sure it's correct and to accurately describe the change in the commit message.

Some things shouldn't have to be explicitly written down but here we are... 😩

✅ Onkel werden

Databases of structured motivated proofs. ~ Timothy Gowers, Anand Rao, Anshula Gandhi, Jacob Loader, Jovan Gerbscheid, Jonas Bayer. https://www.renaissancephilanthropy.org/databases-of-structured-motivated-proofs #AI #Math #ITP #LeanProver

Hello

Street bunny

Hello

Learn how ICE is getting data from our phones, license plates, even tax data, and why we have to work together to protect our communities, from KQED News and EFF's @cooperqExploit code not people:
https://www.kqed.org/news/12055606/how-ice-is-using-your-data-and-what-you-can-do-about-it

Google is launching a new Google app for Windows experiment in Labs

https://blog.google/products/search/google-app-windows-labs/

#google #windows #search #googlelabs #windows11

Hey there, internet friends. I feel like I make this request maybe once or twice a year, and I know that I generally come up with zilch... but here I go again: do I know *anybody* in New York City with a guest room who likes me enough to host me for a day or two? 😏🤞

It's not that I can't afford a hotel room when I travel. I generally can. But NYC seems uniquely positioned in the world of travel logistics in the sense that you all do not have your garden variety Courtyard Marriott or Doubletree Hilton for around $250/night...

In NYC, travelers seem to be presented with only three choices:

1. the most posh hotel you've ever heard of, for $1000/night at minimum

2. quirky boutique hotel with a 13 sq ft room, for $300/night (no rooms available)

3. battered and firebombed hostel with bunk beds bought at a Dresden fire sale, for $39/night (bag theft included for free)

... I'm just a guy trying to come into town for a weekend to see a play, hah. (And while I appreciate couch offers, I'm over 40 and no longer really do that, please forgive me for being posh)

Document-level autoformalization. ~ Antoine Bosselut, Viktor Kunčak, Maryna Viazovska. https://www.renaissancephilanthropy.org/document-level-autoformalization #AI #Math #ITP #LeanProver #Autoformalization

proposal: make the lifetime single-quote marker in Rust a combining acute accent

before: 'arr, 'num, 'obj (boring, americano-centred)
after: árr, ñum, öbj (delightful, festive, welcoming)

Domain specific (Documentation for Mathlib). ~ John Talbot, Richard M. Hill. https://www.renaissancephilanthropy.org/domain-specific-documentation-for-mathlib-1 #ITP #LeanProver #Mathlib

Shocking news: Tanks are approaching the center of Gaza, and everything is in ruins. All people's dreams are gone. No one knows the pain that will afflict people after their homes are gone. Save what remains of Gaza. We are not numbers.
Our dreams, our days and our homes are gone. Save what remains.😭
#palestine #freepalestine #gaza #famine #extermination #nakba #naksa #shelter #tent #help #helppalestinians #siege

Salzburg "Stadt", wo öffentlicher Verkehr am Hauptbahnhof nach halb acht bestenfalls noch ein 20 Minuten Intervall hat.

寝をしますか
今日もみんなかわいくてありがとう　​​

Game over or QED? (For taking the Lean Game Server to the next level). ~ Marcus Zibrowius. https://www.renaissancephilanthropy.org/game-over-or-qed #ITP #LeanProver

ジムの帰りにおいしいお蕎麦の店を見つけたから良く行くんだけど、たくさん種類があるから次はどれ食べようかな…と毎回楽しみ

GNN-SMT: A consortium based proof automation for Lean 4. ~ Clark Barrett, Leni Aniva, Abdalrhman Mohamed, Harun Khan. https://www.renaissancephilanthropy.org/gnn-smt-consortium-based-proof-automation-for-lean-4 #ITP #LeanProver #SMT

- 구글이 Discover를 업데이트해 트위터, 인스타그램, 유튜브 쇼츠 콘텐츠를 더 보여줌

- 사용자는 크리에이터/퍼블리셔를 직접 팔로우하고 콘텐츠를 미리 볼 수 있음

- 콘텐츠 탐색 중앙화가 목표

Updates to Discover in Search: More content from creators and publishers

https://blog.google/products/search/discover-updates-september-2025/

Interesting essay parsing the difference between blogs and newsletters, and how their delivery mechanisms influence their content and style: https://buttondown.com/blog/blog-vs-newsletter

@nihongomaamaa bold!

Learning to do math with vampires and spiders. ~ Andrei Voronkov, Michael Rawson. https://www.renaissancephilanthropy.org/learning-to-do-math-with-vampires-and-spiders #ITP #LeanProver #Rocq

요즘 여기저기에 AI 기능들이 들어있어서 지금 이 생각밖에 안 듬

패션은 잘 모르지만 오파상(...)으로써 귀동냥한 것 중 가장 호응이 좋았던 것은.
청바지는 🇯🇵의 에비스/모모타로/에드윈.
스트릿과 아메카지(아메리칸 캐쥬얼)은 캐피탈/니들스/(좀 더 어른들은)빔스
조금 더 일반적으로 가면 꼼데가르송/휴먼 메이드
여기서 한 단계 더 올라가면 요지 야마모토의 Ground Y
좀 더 스트릿으로 가면 BAPE
아..아닙니다.

Of these, which is the best cheese for a sandwich?

#EvanPoll #poll

NPMサプライチェーン攻撃のあったtinycolorを含むコンテナイメージを拡張スキャンで検査してみた
https://dev.classmethod.jp/articles/ecr-scan-for-npm-vulnerability/

#dev_classmethod

Scalable theorem proving via mathematical databases. ~ Christopher Birkbeck, David Roe, Andrew Sutherland. https://www.renaissancephilanthropy.org/scalable-theorem-proving #AI #Math #ITP #LeanProver

Huh, spam from 1Password offering me “Early access to Comet, the new AI browser from Perplexity”. I’m perplexed all right, about why 1Password, an outfit I mostly like, is doing this. I want a serious relationship with my security-technology providers, not a spammy one that flirts with sketchy totally-unrelated products.

#genAI #1Password

the big takeaway here — as noted in the article — is that react is too big to vape

https://bogdanthegeek.github.io/blog/projects/vapeserver/

Huh, spam from 1Password offering me “Early access to Comet, the new AI browser from Perplexity”. I’m perplexed all right, about why 1Password, an outfit I mostly like, is doing this. I want a serious relationship with my security-technology providers, not a spammy one that flirts with sketchy totally-unrelated products.

#genAI #1Password

파도타기 하다보면 팔로우할만한 사람들이 이렇게나 많은데...!! 라는 심정으로 트위터에 연합우주 계정 정리하는 타래 적고 있음 https://x.com/kodingwarrior/status/1965606406507430247

꾸준함이 변화를 만들어낸다...!!!

Alright, buckle up internet history fans: we've come to the RSS Format Wars! The year 2000 was when RSS got forked into 2 different protocols: Dave Winer's RSS 0.92 and the RDF-based RSS 1.0. What's remarkable, looking back, is that the top bloggers of the day — Kottke, CamWorld, Rebecca Blood, Brad Graham, and others — still weren't using RSS by the end of that year. But they *were* building blogrolls. https://cybercultural.com/p/blogs-rss-2000/ #InternetHistory #RSS

Sketchpad: A high-precision and easy-to-use system for automatic formal sketch generation. ~ Wenda Li, Luo Mai, Larry Paulson, Huajian Xin. https://www.renaissancephilanthropy.org/sketchpad-a-high-precision-and-easy-to-use-system-for-automatic-formal-sketch-generation #AI #Math #ITP #IsabelleHOL #LeanProver