I don't trust Lean code from AI

> And an AI that is bound to find bugs and exploit them (rather than disclose them), is extremely problematic as a certificate.

If the AI found a bug, it would use it to prove any kind of stuff and we would get 700 new publications per day.