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

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.