Hacker News Reader

moonseton 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!

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