Zulip Chat Archive

Stream: new members

Topic: Undergrad calculus


wanaks (Jan 31 2023 at 19:03):

Hi everyone. I took undergraduate calculus a long time ago and consider myself quite rusty. I've been meaning to work through Spivak's Calculus to build that knowledge back up. I also have been meaning to play around with Lean. I'm toying around with the idea of using Lean to work through Spivak's material, but I don't remember enough about calculus and don't know enough about Lean and the capabilities of mathlib to have an idea of whether such an exercise would be futile. Any thoughts on the matter would be appreciated.

Kevin Buzzard (Jan 31 2023 at 19:06):

I would give it a go. I'm sure you'll learn something!

wanaks (Jan 31 2023 at 19:24):

Thanks for the input. I know mathlib is an actively developed project. Do you think the library has enough support for this exercise? Or are there certain topics, for which mathlib might not currently have the functionality that I will need, of which I should be aware?

Kevin Buzzard (Jan 31 2023 at 19:30):

Which bits of Spivak were you thinking of formalising? You can always search the mathlib docs https://leanprover-community.github.io/mathlib_docs/

wanaks (Jan 31 2023 at 19:53):

No specific bits. I was planning on working through it cover-to-cover and using lean to either reconstruct proofs included in the text or write solutions to the exercise questions that ask for proofs.

Martin Dvořák (Jan 31 2023 at 19:56):

That's a LOT of work!

Gareth Ma (Jan 31 2023 at 20:08):

Working on formalising the exercise statements might be interesting though, and might be useful for other classes or students? :thinking:

wanaks (Jan 31 2023 at 20:11):

Martin Dvořák said:

That's a LOT of work!

Yes, I suspect I’ll need to be judicious in exercise selection. My experience with Lean is limited, so I’m likely underestimating the level of effort for writing the proofs as well (only one way to find out).


Last updated: Dec 20 2023 at 11:08 UTC