that sounds awesome! what does the process of getting to one of those proofs look like? is there a lot of back and forth, or is it mostly autonomous?

Mostly autonomous, with a bit of guidance, but this might be because the training set has examples that are similar enough, making interpolation easy.

fantastic! i hope you decide to share more details; i'd love to hear them

Thanks. It's a toy at the minute, there is nothing super impressive.

Taking this forward would require a lot more work and funding to pay for computation to fine-tune models further.

It's an interesting topic, perhaps good for a startup or a research lab in case one finds a decent monetization stream.

pretty sure you'll be able to monetize writing correct software at scale with an llm