The title doesn’t capture the whole article, it talks about wiring up SAT solvers to LLMs and how that might help solve difficult math problems. The proofs will be difficult or impossible to understand as a human, but:

Heule argues that most mathematicians overvalue understanding and undervalue trust.