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

	▲	therealdrag0 an hour ago \| parent [-]
		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.