6gvONxR4sf7o

It's interesting to think about this expanded view of religion and how it interacts with nondiscrimination laws. The guy's beliefs (at least in the quotes in the article) seem like a good combination of well reasoned and sensible and core faith-like beliefs, so I'm glad they're protected. At the same time, I can imagine plenty of beliefs that would make me not want to hire someone. I know this one didn't go to court, but I wonder what tests courts use to draw the lines. What deeply held beliefs am I allowed to say make someone an idiot or jerk I don't want to hire, and what deeply held beliefs am I allowed to hold and want the state to protect?

It's wild seeing opus 5.5 up there so high, while i'm still using Fable 5.1 because I couldn't stand how opus writes.

I think it means if we all have to justify ourselves to each other, we collectively come up with an sustainable ecosystem of ideas that we can understand. So if we stop justifying ourselves to each other, the ecosystem doesn't get built or sustained, and we stop understanding things. Not the person you responded to, but that's my reading.

I hope that eventually choreographic programming is baked into language runtimes to the point that it feels like manually placing certain data on certain parts of RAM/cache. It's one of those ideas that's great, but manual implementations always seem like a mess.

> PEP 798: Unpacking in comprehensions

> PEP 814: Add frozendict built-in type

About damned time. These are little quality of life changes that I've wanted roughly forever. Glad to see them arriving.

It's a funny feeling being on the outside of this with a background in applied math, not pure math. There are all these AI results in pure math, and pure mathematicians worrying about the role of mathematicians and looking for new purpose, meanwhile applied math is sitting here much less affected. From my perspective, the answer seems obvious.

My hope is that applied math departments and pure math departments get closer, and that we start having a ton more people finding applications outside of pure math for pure math results.

Lean compiles its code to C, so it's pretty good on that end of the spectrum, though it does have a bit of a runtime, so it's certainly not at the very end of spectrum where Rust/C/C++ are (never used Go, so idk). With some optimization my personal experience is that it's not that bad to get it within a factor of 2-5 of half-decent rust speed. My personal mental model of it is like a more-to-my-tastes wildly-faster python but without an ecosystem.

As for library support, yeah it's definitely not a mature ecosystem. But since it compiles to C, the FFI is great, so you can just ask an LLM to write bindings to your favorite rust/C/C++ library and they do just fine. I recently wanted (apache) arrow bindings for lean, and LLMs knocked out perfectly sufficient bindings just fine.

You might be interested in Lean. It's my favorite lisp, even though it's really not at all a lisp. It's a nice programming language, and it lets you really hack on commands, macros, syntax, and elaboration.

I think you're misreading Lean Web. Over on the right side with that you'll see:

    `Real` has already been declared

for your `abbrev Real`, and you'll see our Application type mismatch: The argument Complex.I has type ℂ but is expected to have type ℝ in the application Exists.intro Complex.I

for the first term in your `exact` brackets.

It means that it rejects the proof. I suspect it may have been because you came back to the page too long after opening it, at which point you'll see `Lean server has stopped.` and won't get any type checking at all on Lean Web until you refresh.

But if I understand the point you're trying to make, that if you did shadow the name Real to actually mean Complex, then it would check, then yeah you're correct. But that's still where you just have to understand the statement, not the proof. The statements are never the giant 500k LoC part.

In a fixed version of your example, that means

- it's on you to understand that the statement unpacks to `∃ x : ℂ, x * x = -1`

- it's on you to look at whether the proof checker allows the proof (and potentially with what axioms, depending on your level of care)

- it's not on you to understand the proof

Much of the point is that you have to understand the lean statement, not its proof. If the proof checker says it's good and reports that it just uses the usual axioms, then you can trust that they imply the statement. And the statement is never the 500k line part.

What a shame that the focus in the article seems to be on "winning." Seems like winning comes first and safety comes second, and the only question is how far apart they are. That's not surprising, but also not encouraging.

Seems like a very choosy headline, given the rest of his comments. It's a tiny 13 sentence article, and more interesting than the headline. Unsurprising which line they picked for the headline, but disappointing.

> But why subscription for local-only software?

I assume that they decided the business model and user experience separately. It's generally harder to build local-only software than stuff that just uses the cloud for all the hard work, but it's a better user experience. I'd be willing to pay more for local-first, but yeah it certainly does feel weird.

My experience has been the opposite. If lean had linear types (or separation types), it would be, but as it is, Lean's just a little bit too focused on talking about results to tidily talk about how those results are computed.