gaogao

7 ms·

1.
by gaogao 1mo ago
Do you have any personal stake in the enterprise?
2.
by gaogao 1mo ago
Frequent minor version bumps are pretty common these days. Opus 4.7 -> 4.8 was 42 days.
3.
by gaogao 7mo ago
Doesn't |& work with bash?
4.
by gaogao 7mo ago
Nah, the articles are non-contradicting. That article focuses on how the spend mostly goes to imports, which decreases GDP. This one focuses on the effects on unemployment. It's very plausible that a decrease in interest rates right no
5.
by gaogao 7mo ago
Yes, though often the easiest way to replicate it in regular programming languages is to translate that language to Lean or another ITM, though auto-active like Verus is used for Rust pretty successfully. Python and C though have enough nas
6.
by gaogao 7mo ago
The future is now. The recent couple of Lean releases have leaned more on software verification, I believe in part due to Amazon hiring a number of the core devs.
7.
by gaogao 7mo ago
Yeah, I pointed a custom thing and Claude at #6, and it's solved it in Lean besides needing to axiomize one theorem not in mathlib. Only about four of the problems have enough foundations formalized in mathlib though for this approach.
8.
by gaogao 9mo ago
The compiler for CUDA Tile being Blackwell only is a baffling decision. I wanted to try it out, but it's only really easy to grab H100s quickly right now. I guess maybe I'll try it out on my 5070 Ti after traveling, but am more li
9.
by gaogao 9mo ago
Yup, I've already spent like $20k using Claude to verify things, so like there's probably some room for cost cutting.
10.
by gaogao 9mo ago
Yeah, Rust has been pretty good for formal verification so far. Hoare spec contracts I think are the way forward, especially since they fairly naturally flow from unittests. I've been using Hax to pretty good effect so far. I'm ge
11.
by gaogao 9mo ago
Topical to my interests, I used Claude Code the other day for formally verifying some matrix multiplication in Rust. Writing the spec wasn't too hard actually, done as post-conditions in code, as proving equivalence to a simpler versio
12.
by gaogao 9mo ago
> Season 8: In this season, they introduced gender fluidity. Whilst an interesting problem on its own, this would have wreaked havoc on my model. Well I guess free money except for that one. In that one, one of the contestants, Danny, di
13.
by gaogao 10mo ago
Pathways, I understand, is more so these days just the name for their training orchestrator for doing distributed JAX stuff - https://github.com/google/pathways-job
14.
by gaogao 10mo ago
The gaps that led to this was, I think, part of why the CISO got replaced - https://www.thestack.technology/anthropic-new-ciso-claude-cy...
15.
by gaogao 10mo ago
> In 2007, the scientist, who once worked at the University of Cambridge's Cavendish Laboratory, told the Times newspaper that he was "inherently gloomy about the prospect of Africa" because "all our social policies a
16.
by gaogao 10mo ago
If asked non-directly, it still currently answers it - https://www.kimi.com/share/19a5ab4a-e732-8b8b-8000-00008499c...
17.
by gaogao 11mo ago
Ah so, this is pretty possible, as it's a flavor of text adventure puzzle that usually shows up every year or two for Mystery Hunt. I agree that visually allows this to a greater degree, but it's exceedingly doable to have such a
18.
by gaogao 11mo ago
Oh also good talk at PTC yesterday! I had meant to ask you more about the formal memory model, but the other post talk questions ended up being really interesting too.
19.
by gaogao 11mo ago
Yup, hyperreactor, one of the new crates that's part of it, does some particularly interesting things for efficient parallel distributed channels.
20.
by gaogao 11mo ago
> It's a pity they don't do a complete rewrite with a functional language as the driver. It's open source, so seeing such an extension would be quite cool. There's much that could be done with native Rust actors and c
21.
by gaogao 11mo ago
> As far as things that might be a performance loss here, one thing I'm wondering is if custom kernels are supported Yeah, you might end up needing some changes to remote worker initialization, but you can generally bake in whatever
22.
by gaogao 11mo ago
Nah, focusing on a different controller paradigm. Jax is focused on multi-controller SPMD, while this is focused on a single-controller setup. Both have their place, with single-controller being generally easier to reason about, and multi-c
23.
by gaogao 11mo ago
Yup, there's stuff like https://pytorch.org/blog/introducing-torchforge/ on top of it now
24.
by gaogao 11mo ago
Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
25.
by gaogao 11mo ago
Yeah, I don't think surrealism or constructed is good in the early data mix, but as part of mid or post-training seems generally reasonable. But also, this is one of those cases where anthropomorphizing the model probably doesn't
26.
by gaogao 11mo ago
Brain rot texts seems reasonably harmful, but brain rot videos are often surreal and semantically dense in a way that probably improves performance (such as discussed on this German brain rot analysis https://www.youtube.com&#x2F
27.
by gaogao 1y ago
Iffy by the headline, but the every-other-week model doesn't sound absolutely the worst. I don't have a great read on if it's a bad idea or not though.
28.
by gaogao 1y ago
Yeah, it's under "Non-SI units accepted for use with SI", so more ISO than SI, but has standards for how it's used with SI units, esp since M has meaning there
29.
by gaogao 1y ago
Yeah, the SI symbol for minutes is min, if you're going to abbreviate it in a technical context. Super funky using M.
30.
by gaogao 1y ago
> I wonder if we'll ever use AI to write code in dependently typed languages Yeah, I write code in Lean with AI pretty frequently lately

More ›