← Back to context

Comment by est31

9 hours ago

Which models do you see to be productive for the task of writing lean? Big fan of pgrust.

I've been using Opus 5.5 for pretty much everything

I tried giving Astra a shot. Since it scores better on math, I thought it might do better at writing Lean. I forgot the exact details, but that didn't end up being the case. I think it wasn't thinking holistically enough and tended to rabbit hole itself more

  • Opus 5.5 is a god tier model, but for serious large scale work, nothing beats getting at least three non-similar models to repeatedly refine a super detailed plan before any code is written.

    Right now my consortium is Opus 5.5, Grok 4.7 and Muse Wonder. These three are different enough that their insights are very complementary. Once a plan is detailed enough, any decent model can execute on it successfully, but I personally like Grok’s ability to stick to the plan. (And no 5-hour quota!)

    • Always fascinating to see Grok marketing in the wild. Always the same pattern of mentioning it innocently at the beginning of the message, then doubling down with a specific praise at the end. Well it's rare enough that it could also be a set of users who organically made it their mission to get HN to care about Grok.

      3 replies →

  • Same experience on my vibe coding side project. Astra seems autistic to the context, Claude seems more of an open minded partner with good taste.