definite and indefinite integrals on the reals

Stream: Is there code for X?

[Kevin Buzzard]

Can we prove

$\int_{t=0}^1t^2\mathrm{d}t=\frac{1}{3}$

or

$\int_{t=1}^x\frac{\mathrm{d}t}{t}=\log(x)$

for $x>0$?

I'm sorry to use this stream for these questions. I haven't been keeping up with analysis at all and it's been moving fast. I am just looking at what our undergraduates do in their methods course and am wondering how much of it we can currently formalise.

[Kevin Buzzard]

PS I am not sure that I care which theory of integration one uses here, I am just looking for something which looks to a mathematician like it might say one of the theorems above.

[Patrick Massot]

No, there is a stuck PR that would allow to do that, but the author disappeared.

[Yury G. Kudryashov]

I can take over this PR once I'm done grading the exam.

[Yury G. Kudryashov]

If @Jeremy Avigad will say that it's OK.

[Yury G. Kudryashov]

Jeremy says that a couple of weeks ago @Joe said that he's going to come back to these PRs.

[Jeremy Avigad]

Yes, it is o.k. with me. I asked Joe to coordinate, so hopefully he will respond to the ping.