moonset

Re:Leanstral 1.5: Proof Abundance for All on Saturday July 04, 2026 @01:21PM (#48787075)

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!

Re:Leanstral 1.5: Proof Abundance for All on Friday July 03, 2026 @08:37PM (#48781601)

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.