<rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Hacker News: gaogao</title><link>https://news.ycombinator.com/user?id=gaogao</link><description>Hacker News RSS</description><docs>https://hnrss.org/</docs><generator>hnrss v2.1.1</generator><lastBuildDate>Mon, 06 Apr 2026 07:05:06 +0000</lastBuildDate><atom:link href="https://hnrss.org/user?id=gaogao" rel="self" type="application/rss+xml"></atom:link><item><title><![CDATA[New comment by gaogao in "What does " 2>&1 " mean?"]]></title><description><![CDATA[
<p>Doesn't |& work with bash?</p>
]]></description><pubDate>Fri, 27 Feb 2026 02:05:03 +0000</pubDate><link>https://news.ycombinator.com/item?id=47175411</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=47175411</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47175411</guid></item><item><title><![CDATA[New comment by gaogao in "Fed's Cook says AI triggering big changes, sees possible unemployment rise"]]></title><description><![CDATA[
<p>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 now would lead to more imports and AI spending, not increased employment.</p>
]]></description><pubDate>Wed, 25 Feb 2026 00:49:37 +0000</pubDate><link>https://news.ycombinator.com/item?id=47145810</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=47145810</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47145810</guid></item><item><title><![CDATA[New comment by gaogao in "Lean 4: How the theorem prover works and why it's the new competitive edge in AI"]]></title><description><![CDATA[
<p>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.<p>Python and C though have enough nasal demons and undefined behavior that it's a huge pain to verify things about them, since some random other thread can drive by and modify memory in another thread.</p>
]]></description><pubDate>Sat, 21 Feb 2026 09:06:26 +0000</pubDate><link>https://news.ycombinator.com/item?id=47098892</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=47098892</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47098892</guid></item><item><title><![CDATA[New comment by gaogao in "Learning Lean: Part 1"]]></title><description><![CDATA[
<p>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.</p>
]]></description><pubDate>Thu, 19 Feb 2026 04:32:04 +0000</pubDate><link>https://news.ycombinator.com/item?id=47069944</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=47069944</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47069944</guid></item><item><title><![CDATA[New comment by gaogao in "First Proof"]]></title><description><![CDATA[
<p>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.</p>
]]></description><pubDate>Sun, 08 Feb 2026 12:09:27 +0000</pubDate><link>https://news.ycombinator.com/item?id=46933582</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=46933582</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46933582</guid></item><item><title><![CDATA[New comment by gaogao in "CUDA Tile Open Sourced"]]></title><description><![CDATA[
<p>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 likely to stick to an IR that targets multiple platforms, since they couldn't be bothered.</p>
]]></description><pubDate>Fri, 26 Dec 2025 13:08:39 +0000</pubDate><link>https://news.ycombinator.com/item?id=46391640</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=46391640</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46391640</guid></item><item><title><![CDATA[New comment by gaogao in "Test, don't just verify"]]></title><description><![CDATA[
<p>Yup, I've already spent like $20k using Claude to verify things, so like there's probably some room for cost cutting.</p>
]]></description><pubDate>Tue, 23 Dec 2025 17:08:29 +0000</pubDate><link>https://news.ycombinator.com/item?id=46366996</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=46366996</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46366996</guid></item><item><title><![CDATA[New comment by gaogao in "Test, don't just verify"]]></title><description><![CDATA[
<p>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 generally suspect that advances in Lean proof solving by dedicated models are that useful for program verification, compared to generalist models, though it could help lower costs a good bit.</p>
]]></description><pubDate>Tue, 23 Dec 2025 17:05:22 +0000</pubDate><link>https://news.ycombinator.com/item?id=46366961</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=46366961</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46366961</guid></item><item><title><![CDATA[New comment by gaogao in "AI will make formal verification go mainstream"]]></title><description><![CDATA[
<p>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 version of the code, such as for optimization, is pretty straight forward. Maybe I should write up a proper post on it.</p>
]]></description><pubDate>Tue, 16 Dec 2025 23:26:27 +0000</pubDate><link>https://news.ycombinator.com/item?id=46296162</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=46296162</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46296162</guid></item><item><title><![CDATA[New comment by gaogao in "“Are you the one?” is free money"]]></title><description><![CDATA[
<p>> Season 8: In this season, they introduced gender fluidity. Whilst an interesting problem on its own, this would have wreaked havoc on my model.<p>Well I guess free money except for that one. In that one, one of the contestants, Danny, did the math for optimizing their remaining Truth Booths and Match Ups to get it down to a 50/50 shot.</p>
]]></description><pubDate>Mon, 15 Dec 2025 21:49:40 +0000</pubDate><link>https://news.ycombinator.com/item?id=46281215</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=46281215</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46281215</guid></item><item><title><![CDATA[New comment by gaogao in "Gemini 3 Pro Model Card [pdf]"]]></title><description><![CDATA[
<p>Pathways, I understand, is more so these days just the name for their training orchestrator for doing distributed JAX stuff - <a href="https://github.com/google/pathways-job" rel="nofollow">https://github.com/google/pathways-job</a></p>
]]></description><pubDate>Tue, 18 Nov 2025 21:42:08 +0000</pubDate><link>https://news.ycombinator.com/item?id=45972567</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45972567</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45972567</guid></item><item><title><![CDATA[New comment by gaogao in "Disrupting the first reported AI-orchestrated cyber espionage campaign"]]></title><description><![CDATA[
<p>The gaps that led to this was, I think, part of why the CISO got replaced - <a href="https://www.thestack.technology/anthropic-new-ciso-claude-cyber-attack/" rel="nofollow">https://www.thestack.technology/anthropic-new-ciso-claude-cy...</a></p>
]]></description><pubDate>Thu, 13 Nov 2025 19:58:05 +0000</pubDate><link>https://news.ycombinator.com/item?id=45919722</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45919722</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45919722</guid></item><item><title><![CDATA[New comment by gaogao in "James Watson has died"]]></title><description><![CDATA[
<p>> 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 are based on the fact that their intelligence is the same as ours - whereas all the testing says not really".<p>> While his hope was that everybody was equal, he added, "people who have to deal with black employees find this is not true".<p>Yeah, pretty racist</p>
]]></description><pubDate>Fri, 07 Nov 2025 22:24:38 +0000</pubDate><link>https://news.ycombinator.com/item?id=45851903</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45851903</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45851903</guid></item><item><title><![CDATA[New comment by gaogao in "Kimi K2 Thinking, a SOTA open-source trillion-parameter reasoning model"]]></title><description><![CDATA[
<p>If asked non-directly, it still currently answers it -  <a href="https://www.kimi.com/share/19a5ab4a-e732-8b8b-8000-00008499c36e" rel="nofollow">https://www.kimi.com/share/19a5ab4a-e732-8b8b-8000-00008499c...</a></p>
]]></description><pubDate>Thu, 06 Nov 2025 19:47:25 +0000</pubDate><link>https://news.ycombinator.com/item?id=45839471</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45839471</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45839471</guid></item><item><title><![CDATA[New comment by gaogao in "Blue Prince (1989)"]]></title><description><![CDATA[
<p>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 layered game just in text.</p>
]]></description><pubDate>Wed, 05 Nov 2025 17:59:49 +0000</pubDate><link>https://news.ycombinator.com/item?id=45825844</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45825844</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45825844</guid></item><item><title><![CDATA[New comment by gaogao in "Show HN: Cuq – Formal Verification of Rust GPU Kernels"]]></title><description><![CDATA[
<p>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.</p>
]]></description><pubDate>Thu, 23 Oct 2025 13:41:00 +0000</pubDate><link>https://news.ycombinator.com/item?id=45681712</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45681712</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45681712</guid></item><item><title><![CDATA[New comment by gaogao in "PyTorch Monarch"]]></title><description><![CDATA[
<p>Yup, hyperreactor, one of the new crates that's part of it, does some particularly interesting things for efficient parallel distributed channels.</p>
]]></description><pubDate>Thu, 23 Oct 2025 13:39:33 +0000</pubDate><link>https://news.ycombinator.com/item?id=45681694</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45681694</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45681694</guid></item><item><title><![CDATA[New comment by gaogao in "PyTorch Monarch"]]></title><description><![CDATA[
<p>> It's a pity they don't do a complete rewrite with a functional language as the driver.<p>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 code that get maybe at what you want, but nothing precludes mixing PyTorch and other backends.<p>For example, you could wrap a C++ inference engine as part of one of the actors generating data for other actors doing distributed training.</p>
]]></description><pubDate>Thu, 23 Oct 2025 13:36:35 +0000</pubDate><link>https://news.ycombinator.com/item?id=45681658</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45681658</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45681658</guid></item><item><title><![CDATA[New comment by gaogao in "PyTorch Monarch"]]></title><description><![CDATA[
<p>> As far as things that might be a performance loss here, one thing I'm wondering is if custom kernels are supported<p>Yeah, you might end up needing some changes to remote worker initialization, but you can generally bake in whatever kernels and other system code you need.</p>
]]></description><pubDate>Thu, 23 Oct 2025 13:32:31 +0000</pubDate><link>https://news.ycombinator.com/item?id=45681619</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45681619</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45681619</guid></item><item><title><![CDATA[New comment by gaogao in "PyTorch Monarch"]]></title><description><![CDATA[
<p>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-controller more optimal for certain dataflows. There's also some interesting mixes of the two control paradigms.</p>
]]></description><pubDate>Thu, 23 Oct 2025 13:28:20 +0000</pubDate><link>https://news.ycombinator.com/item?id=45681580</link><dc:creator>gaogao</dc:creator><comments>https://news.ycombinator.com/item?id=45681580</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45681580</guid></item></channel></rss>