It's getting cheaper and cheaper to generate corpora by the day, and Agda has the advantage of being verifiable like Lean. So you can simulate large amounts of programs and feed these back into the model. I think this is a major reason why we're seeing remarkable improvements in formal sciences like the recent IMO golds, and yet LLMs are still struggling to generate aesthetically pleasing and consistent CSS. Imagine a high schooler who can win an IMO gold medal but can't center a div!
It seems like "generating" a corpus in that situation is more like a search process guided by prompts and more critically the type checker, rather than a straight generation process right? You need some base reality or you'll still just have garbage in, garbage out.
