Undergrad calculus

Stream: new members

[wanaks]

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]

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

[wanaks]

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]

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

[wanaks]

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]

That's a LOT of work!

[Gareth Ma]

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

[wanaks]

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).