Zulip Chat Archive

Stream: maths

Topic: integrals and pi


view this post on Zulip 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 2111x2dx=π2 \cdot \int_{-1}^1 \sqrt{1 - x^2}\, \mathrm{d}x = \pi?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 24 2020 at 20:40):

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

view this post on Zulip Yury G. Kudryashov (Jan 25 2020 at 00:58):

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

view this post on Zulip Mario Carneiro (Jan 25 2020 at 01:07):

This is a 100 theorem FYI

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 01:09):

This would be a really nice milestone

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 01:10):

Can we produce a nice mathematician-readable proof?

view this post on Zulip Mario Carneiro (Jan 25 2020 at 01:10):

I doubt it

view this post on Zulip Mario Carneiro (Jan 25 2020 at 01:10):

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

view this post on Zulip Mario Carneiro (Jan 25 2020 at 01:11):

You mean of FTC or the circle?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 01:13):

Oh I'm talking about the circle!

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 01:13):

A nice calc proof or something

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 25 2020 at 01:16):

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

view this post on Zulip Mario Carneiro (Jan 25 2020 at 01:17):

which works for the majority of calc 1 style problems

view this post on Zulip 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