Can someone please tell Leo that these obviously LLM-generated blog posts are cringe? https://leodemoura.github.io/blog/2026-4-2-why-lean/
Why Lean? — Leonardo de Moura

Leonardo de Moura — Creator of Lean and Z3

@zwarich oh my god I thought you were joking

@jonmsterling @zwarich To me it's cringe, but it isn't that it sounds LLM-generated so much as that it's the kind of machismo writing style that sounds engineered in a lab to get HN upvotes. But maybe that's not all that different.

Who is the "No obscure compiler for a dead language" line supposed to be negging?

@lindsey @jonmsterling @zwarich Isabelle and its SML implementation?
@mevenlennonbertrand @lindsey @zwarich I’ll have to ask Larry about this next time I see him. The thing I like about Larry is he writes his own fucking blog posts 😂😂😂
@pigworker @mevenlennonbertrand @lindsey @zwarich Yeah, Larry is so Larry that he is one of a kind. I really treasure every moment I spend with him.
@pigworker @mevenlennonbertrand @lindsey @zwarich By the way, once upon a time I created a very unhinged image. I wonder if Leo would like to use it for his next blog post? This was back in the day when to make stupid propaganda images, we did things like draw pictures with our hands.
@jonmsterling He had left type theory before I arrived, so I don't know him as well as I should like. Always food for thought. @mevenlennonbertrand @lindsey @zwarich
Poly/ML Home Page

@zwarich @mevenlennonbertrand @lindsey @jonmsterling I've been playing with it for the past month or so. It's obviously not "modern" ( no utf8 support, package manager etc) but still pretty nice and def not dead in terms of commit activity.