# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: definite and indefinite integrals on the reals

#### Kevin Buzzard (Apr 13 2020 at 22:19):

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 (Apr 13 2020 at 23:00):

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 (Apr 14 2020 at 07:52):

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

#### Yury G. Kudryashov (Apr 14 2020 at 17:38):

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

#### Yury G. Kudryashov (Apr 14 2020 at 19:09):

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

#### Yury G. Kudryashov (Apr 14 2020 at 19:10):

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

#### Jeremy Avigad (Apr 14 2020 at 19:18):

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

Last updated: May 07 2021 at 19:12 UTC