Mathematicians struggle with the same problem as software engineers; you can let AI generate the artifact, but to understand fully what is going on is challenging. Perhaps even more for mathematicians.

Do you rely on the tests/Lean to accept correctness or not…