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
loading story #50204818
loading story #50203871