Hacker News: 6gvONxR4sf7o

New comment by 6gvONxR4sf7o in "I know why the mathematicians weep"

6gvONxR4sf7o — Thu, 15 Oct 2026 18:17:55 +0000

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.

New comment by 6gvONxR4sf7o in "Choreographic Programming in Rust"

6gvONxR4sf7o — Mon, 12 Oct 2026 16:45:13 +0000

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.

New comment by 6gvONxR4sf7o in "Python 3.15"

6gvONxR4sf7o — Fri, 09 Oct 2026 16:53:58 +0000

> 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.

New comment by 6gvONxR4sf7o in "“Math 2.0” will need to value mathematical progress more holistically"

6gvONxR4sf7o — Thu, 08 Oct 2026 16:51:59 +0000

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.

New comment by 6gvONxR4sf7o in "Why Common Lisp is now the best programming language"

6gvONxR4sf7o — Tue, 06 Oct 2026 20:21:35 +0000

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.

New comment by 6gvONxR4sf7o in "Why Common Lisp is now the best programming language"

6gvONxR4sf7o — Tue, 06 Oct 2026 04:42:45 +0000

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.

New comment by 6gvONxR4sf7o in "Anatomy of a Lean proof for software engineers"

6gvONxR4sf7o — Sun, 04 Oct 2026 02:24:14 +0000

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

New comment by 6gvONxR4sf7o in "Anatomy of a Lean proof for software engineers"

6gvONxR4sf7o — Sat, 03 Oct 2026 01:10:14 +0000

Honestly, I'd say just play some of the lean games instead (https://adam.math.hhu.de/). I went through the dependent type theory and proof stuff first, and in hindsight it would have been much faster to just get the intuition first from learning to use a language like lean.

New comment by 6gvONxR4sf7o in "Anatomy of a Lean proof for software engineers"

6gvONxR4sf7o — Sat, 03 Oct 2026 01:07:10 +0000

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.

New comment by 6gvONxR4sf7o in "FTC is investigating OpenAI, Anthropic and other AI companies over product risks"

6gvONxR4sf7o — Thu, 01 Oct 2026 15:51:04 +0000

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.

New comment by 6gvONxR4sf7o in "Nicolas Cage Says the MCU 'Is Becoming a Well-Funded and Glorified WWE'"

6gvONxR4sf7o — Thu, 01 Oct 2026 15:37:30 +0000

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.

New comment by 6gvONxR4sf7o in "Ink and Switch interactive homepage"

6gvONxR4sf7o — Fri, 25 Sep 2026 16:04:48 +0000

> 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.

New comment by 6gvONxR4sf7o in "Book review: Is parallel programming hard, and, if so, what can you do about it?"

6gvONxR4sf7o — Thu, 24 Sep 2026 21:15:40 +0000

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.

New comment by 6gvONxR4sf7o in "Advisory Group on Mathematics and Artificial Intelligence"

6gvONxR4sf7o — Mon, 21 Sep 2026 23:27:04 +0000

> The group will operate independently from OpenAI. The group will have the freedom to offer advice we have not requested, comment on OpenAI’s impact on mathematics, and make its advice public.

That seems so empty. I also operate independently from them and have the freedom to tell them things they haven't requested and comment on their impact and do so publicly. But I doesn't have any impact on OpenAI. If they're trying to say how this will actually have any impact on anything at all, they're doing a shit job.

New comment by 6gvONxR4sf7o in "Fable 5 – Median thinking declined in August"

6gvONxR4sf7o — Mon, 21 Sep 2026 17:58:04 +0000

That's like the entire field of statistics.

New comment by 6gvONxR4sf7o in "Hugging Face is billing OpenAI $100M for hacking it"

6gvONxR4sf7o — Tue, 15 Sep 2026 19:22:38 +0000

I wonder if it's in openai's interest to play nice here. They can't have a precedent of "the future is we do whatever we want with no consequences for screwing up" if they want public interest on their side, but they also can't have "you (our customers) will be held accountable for what you're paying us to do if we screw up." And that's before the IPO interests even come in.

New comment by 6gvONxR4sf7o in "Experiment – Projectional Viewer"

6gvONxR4sf7o — Fri, 11 Sep 2026 16:16:21 +0000

I'd bet that it needs a better abstraction like LSP. IDEs are super expensive to build, so an IDE company isn't going to try to abstract away their business, so it's a long time between LSP-like developments, and I can imagine something that would enable that sort of thing needing to be a couple major breaking versions of LSP away from where we are, at minimum, which would mean a decade or two from existing across the ecosystem, at the least.

New comment by 6gvONxR4sf7o in "The Waymo effect: how AI is quietly making research less collaborative"

6gvONxR4sf7o — Fri, 11 Sep 2026 16:08:51 +0000

I'd bet it depends on what they write to the LLM, since sycophancy is so strong in these things. If they write in a fairly agnostic way, it might default to sycophancy to you the dev, while if they write it in an opinionated way it might default to sycophancy to them. Regardless of who is right.

New comment by 6gvONxR4sf7o in "Navier-Stokes – Tristan Buckmaster [pdf]"

6gvONxR4sf7o — Tue, 08 Sep 2026 22:41:05 +0000

Is this the future we're headed towards? Where I'll be afraid to use google docs in case Google identifies value in whatever I'm writing about and snipes it if it my docs make it into the next round of model training?

New comment by 6gvONxR4sf7o in "An Alien Mind"

6gvONxR4sf7o — Mon, 07 Sep 2026 01:53:14 +0000

> Automated AI research is a more dramatic form of scaling intelligence with compute; and of course as a part of it, AI will improve the computational substrate itself . And similarly to scaling, we focus OpenAI research towards RSI as we believe it is the only way to remain at the frontier of AI research moving forward.

This seems like a terrible idea. The rationale seems to be "we need to do dangerous things as quickly as possible so that we can do them first" or something? I don't agree with that kind of 'if i dont do it someone else will' rationale in general even for otherwise trusted actors, but this is coming from a super untrustworthy org too. I'm super pessimistic about openai's impact on the world here.

Here's to vibe coded alignment, i guess. Vibe alignment?