Assuming you mean “cheaper per unit of token/effort/something”, not cheaper in total to get the Lean code produced.
My understanding from the post, as well as my a priori expectation, is that formalization was a relatively small fraction of the total time/compute spent on this. They threw a fuckton of compute at the agent swarm and then wanted to save by switching to Astra for the final step? IDK, seems implausible.
I would also expect the new model not to be that much more expensive than Astra.
It could also have just been cheaper to use Astra.
Assuming you mean “cheaper per unit of token/effort/something”, not cheaper in total to get the Lean code produced.
My understanding from the post, as well as my a priori expectation, is that formalization was a relatively small fraction of the total time/compute spent on this. They threw a fuckton of compute at the agent swarm and then wanted to save by switching to Astra for the final step? IDK, seems implausible.
I would also expect the new model not to be that much more expensive than Astra.