# How hard is computing integrals in Lean?

Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level integrals, like $$\int_0^1xe^x\,dx$$, and not anything excessively crazy.

Of course, if our goal is merely to have a proof of a statement of the form $$\int_a^bf(x)\,dx=c$$ for some known $$c$$, then proving this in Lean should be possible by finding a function $$F(x)$$, check $$F'(x)=f(x)$$, evaluating $$F(b)-F(a)$$ and appealing to FTC. But this is an approach which is very backwards compared to how this is done by hand (which, at least somewhat implicitly, involves finding such an $$F$$).

My question is, does Lean have any tools which would let you perform such "by hand" calculations within your code? At the very least it would require support for integration by parts and integration by substitution, and I'm not sure those are in mathlib. Ideally I would also imagine some kind of environment like the calc mode.

If not in Lean, are there similar tools available in other proof assistants?

Just to clarify, I do not mean automated computation of integrals like in CAS. I just mean tools which would let you painlessly perform IBP and substitutions (and perhaps other operations) on given integrals to simplify them.

• One of the great advantages of ITPs over CASs is the proof script can encode a witness that might represent a considerable amount of work to produce, without putting that work on the critical path. So while it's certainly possible in principle for Lean to play CAS here and compute the integral itself, I would contend that this is a waste of resources and you should instead precompute (either by Lean or using a CAS) and store the answer and verify it by differentiation. Feb 16, 2022 at 13:55
• I'm curious to know whether there were attempts to formalise parts of Risch algorithm for antiderivative computation. Feb 16, 2022 at 15:43
• The files github.com/leanprover-community/mathlib/blob/master/test/… and github.com/leanprover-community/mathlib/blob/master/test/… are quite interesting examples of elementary integrals in Lean/mathlib. These are fairly compressed, but show that using mathlib and the simplifier/norm_num many basic steps can be automated in tactic mode. This is still regular tactic mode, but one could imagine trying a few different Ansatzen and letting Lean do several calculation steps to correct your antiderivative within this mode. Feb 16, 2022 at 16:10
• for definite integration, there are verified tools: research.vu.nl/en/publications/… Feb 16, 2022 at 21:19