Hacker News: moonsethttps://news.ycombinator.com/user?id=moonsetHacker News RSShttps://hnrss.org/hnrss v2.1.1Tue, 28 Jul 2026 23:19:20 +0000<![CDATA[New comment by moonset in "Leanstral 1.5: Proof abundance for all"]]>Sorry, I recognize that these are different classes of model and didn't mean to punch down. I'm genuinely excited for the work Mistral is doing in this space!

]]>Sat, 04 Jul 2026 17:21:30 +0000https://news.ycombinator.com/item?id=48787075moonsethttps://news.ycombinator.com/item?id=48787075https://news.ycombinator.com/item?id=48787075<![CDATA[New comment by moonset in "Leanstral 1.5: Proof abundance for all"]]>I gave Codex with GPT-5.5 High this prompt:

    Identify bugs in [datrs/varinteger](https://github.com/datrs/varinteger) . Do NOT look at the GitHub issues, just inspect the source
It also found the bug that Leanstral 1.5 found and the authors highlighted. I think this bug wasn't especially tricky; it's just a case of too few eyeballs on this repo.

Congrats on the release regardless! Excited for the direction Lean + automated AI proofs are headed.

Disclosure: I work at OpenAI.

]]>Sat, 04 Jul 2026 00:37:00 +0000https://news.ycombinator.com/item?id=48781601moonsethttps://news.ycombinator.com/item?id=48781601https://news.ycombinator.com/item?id=48781601