Integrating wolfram with chat gpt api works pretty well but your point stands particularly when it comes to logic ; the models might differentiate integrate , work on combinatorics , graph theory ,hell alphatensor even found new linear algebra algorithms but none of em can do any true logic based activities like coming up with original proofs