How do you generate Lean theorems?

[Zhang-Liao]

I am reading your paper. I do not really understand how you generate the Lean theorem statements.
Do you simply use LLM to generate such statements? How do you confirm such theorem statements correspond to the pre/post-condition of a function?

[quinn-dougherty]

thanks for reading! it's a really dumb pipeline. We didn't really see any issues trusting the reliability of the language model in direct translation from hypothesis code to lean statements, though this could've been more rigorous. If anything, the weaknesses of our pipeline was more when the language model inferred hypothesis code (PBTs) from unit tests, this led to some completeness bugs (like a kind of attack surface where people can write code that violates the spirit of a question but passes all the PBTs/theorems).