# Zulip Chat Archive

## 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?

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

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