> For integration we need to prove that such a object exists for each expression we want to integrate before we try integrating.

Can't we just integrate away and check if it's correct by differentiating it back?

EDIT: oh, I guess that's why we need to be able to check for function equality :)

It's been over a decade since I studied it, but from memory you could also end up in infinite loops when you start generating the closed form solution if it doesn't exist. Which with as much hand waving as possible is ultimately equivalent to the computer function form auto integration would produce.

These things seem impossible in theory but in practice you just set a time limit.

Math algorithms are the one area where good enough really isn't good enough.

OK but that's not how automatic differentiation would work?