## Stream: maths

### Topic: integrals and pi

#### Johan Commelin (Jan 24 2020 at 18:38):

I have skimmed over the recent PRs on integrals, and would like to get a feeling for whether we could do some concrete computations now. For example, can we start trying to prove that the area of the circle is pi? More precisely, can we prove $2 \cdot \int_{-1}^1 \sqrt{1 - x^2}\, \mathrm{d}x = \pi$?

#### Patrick Massot (Jan 24 2020 at 20:31):

We don't have anything relating derivatives and integrals, so we are nowhere close to computing an integral.

#### Johan Commelin (Jan 24 2020 at 20:40):

Good point. So this will have to wait for a while...

#### Yury G. Kudryashov (Jan 25 2020 at 00:58):

It's easy to prove FTC now, and Joe is working on this.

#### Mario Carneiro (Jan 25 2020 at 01:07):

This is a 100 theorem FYI

#### Kevin Buzzard (Jan 25 2020 at 01:09):

This would be a really nice milestone

#### Kevin Buzzard (Jan 25 2020 at 01:10):

Can we produce a nice mathematician-readable proof?

I doubt it

#### Mario Carneiro (Jan 25 2020 at 01:10):

I mean you can try to make one but it won't be general enough probably

#### Mario Carneiro (Jan 25 2020 at 01:11):

You mean of FTC or the circle?

#### Mario Carneiro (Jan 25 2020 at 01:12):

For the circle proof, there will be a lot of sidebars but the main line will be recognizable

#### Kevin Buzzard (Jan 25 2020 at 01:13):

Oh I'm talking about the circle!

#### Kevin Buzzard (Jan 25 2020 at 01:13):

A nice calc proof or something

#### Mario Carneiro (Jan 25 2020 at 01:15):

there are a lot of side conditions for each line of the proof, proving that lots of boring stuff is integrable

#### Mario Carneiro (Jan 25 2020 at 01:16):

In metamath I always prove these theorems by writing down an explicit anti-derivative

#### Mario Carneiro (Jan 25 2020 at 01:17):

which works for the majority of calc 1 style problems

#### Mario Carneiro (Jan 25 2020 at 01:18):

the method they teach in school for this stuff makes more sense when you don't know what the answer is and are trying to figure that out concurrently

Last updated: May 12 2021 at 07:17 UTC