integrals and pi

Stream: maths

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

This is a 100 theorem FYI

[Kevin Buzzard]

This would be a really nice milestone

[Kevin Buzzard]

Can we produce a nice mathematician-readable proof?

[Mario Carneiro]

I doubt it

[Mario Carneiro]

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

[Mario Carneiro]

You mean of FTC or the circle?

[Mario Carneiro]

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

[Kevin Buzzard]

Oh I'm talking about the circle!

[Kevin Buzzard]

A nice calc proof or something

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

which works for the majority of calc 1 style problems

[Mario Carneiro]

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