Leanstral 1.5

Discussion about Leanstral 1: https://news.ycombinator.com/item?id=47404796

Real talk, does anyone use anything from Mistral because it performs the best, by whatever secular metric of your choosing? Or is it only used "because EU"? Just focus on answering the question. I wonder if anyone has observed it perform better on any objective metric in any rigorous setting.

Is this useful for specifying programs too or only theorems?

[dead]