This might be a worthy application.

Set to be revolutionized by AI because AI can’t do math.

Says my brother, a Math Professor that works with people trying to develop AI

The article isn’t about automatic proofs, but it’d be interesting to see a LLM that can write formal proofs in Coq/Lean/whatever and call external computer algebra systems like SageMath or Mathematica.

No