Calculus for mathematicians (1997) [pdf] • Hacker News Board

Re: Calculus for mathematicians (1997) [pdf]

#11

Post by bandrami » Thu, May 28, 2015, 9:39 AM UTC

The hardest (ie, best) math prof I ever had (I was in EE, he was in the math department) used to say that "engineers can teach calculus, but their students cannot go on to teach calculus". I'm impressed by someone who knows a subject deeply enough to take that long of a view.

Personally, I just like the engineering view of dx and dy as simply being new variables (with caveats that we immediately forget). Which is why I'll probably not teach calculus any time soon.

But, still, the best "revelation" moment I had was when he off-handedly said "An integral is the inner product of a function and a suitably-dimensioned unit". Light bulb came on, and I "got" integration for the first time. Too bad they can't lead up to it that way in high school.

(Side rant: why do they teach trig before calculus in high school? That's completely backwards. Trig is a bunch of arbitrary formulas if you don't have the calculus behind them.)

Re: Calculus for mathematicians (1997) [pdf]

#12

Post by madez » Thu, May 28, 2015, 9:52 AM UTC

amelius wrote: post #10

How difficult would it be to write this in a formal system? How much space would it take?

You would need to get to the reals, which takes already a fair amount of time and includes a lot of machinery. Depending on how you constructed the reals, you might be able to reuse some concepts. So, it depends on where you start and which path you take.

Also, arguing by reference to the choice of appropriate values is incomplete argumentation and so it won't be accepted by a formal system. You'd have to fill these holes.

I'd suggest to start by evaluating the existing formalized constructions of the reals.

I think it is not too hard.

Re: Calculus for mathematicians (1997) [pdf]

#13

Post by cottonseed » Thu, May 28, 2015, 9:55 AM UTC

amelius wrote: post #10

How difficult would it be to write this in a formal system? How much space would it take?

The Coq standard library formalizes real analysis. Have a look at the "Reals" section:

https://coq.inria.fr/library/

Re: Calculus for mathematicians (1997) [pdf]

#14

Post by eccstartup » Thu, May 28, 2015, 10:12 AM UTC

anon4 wrote: post #9

hudibras wrote: post #4

Definitely stashing this away in my time machine for when I travel back to the 17th century. Make both Leibniz and Newton cry...

If you're taking things like that back in time, make sure to translate them to French. Also, learn French. Not knowing French in the 17th century is like not knowing English today.

I'm learning French. But where is the time machine?

Re: Calculus for mathematicians (1997) [pdf]

#15

Post by jojo3000 » Thu, May 28, 2015, 10:15 AM UTC

amelius wrote: post #10

How difficult would it be to write this in a formal system? How much space would it take?

Even defining the real numbers is already quite involved, for example in Isabelle/HOL it is introduced as quotient over Cauchy sequences:

http://isabelle.in.tum.de/dist/library/HOL/HOL/Real.html

This is the classical way (and similar to HOL Light or HOL4). AFAIK in Coq the standard way is to introduce the reals axiomatically.

The bottom theories in http://isabelle.in.tum.de/dist/library/HOL/HOL/ are all about classical real analysis, based on topology and real-normed vector spaces.

Re: Calculus for mathematicians (1997) [pdf]

#16

Post by mafribe » Thu, May 28, 2015, 10:16 AM UTC

amelius wrote: post #10

How difficult would it be to write this in a formal system? How much space would it take?

Since real analysis is arguably the core of mathematics and of applications of mathematics, it has been formalised in many ways. See [1] for an overview of the state of the art.

[1] S. Boldo, C. Lelay, G. Melquiond, Formalization of Real Analysis: A Survey of Proof Assistants and Libraries., https://hal.inria.fr/hal-00806920v1/document

Re: Calculus for mathematicians (1997) [pdf]

#17

Post by mafribe » Thu, May 28, 2015, 10:20 AM UTC

jojo3000 wrote: post #15

amelius wrote: post #10

How difficult would it be to write this in a formal system? How much space would it take?

Even defining the real numbers is already quite involved, for example in Isabelle/HOL it is introduced as quotient over Cauchy sequences: http://isabelle.in.tum.de/dist/library/HOL/HOL/Real.html This is the classical way (and similar to HOL Light or HOL4). AFAIK in Coq the standard way is to introduce the reals axiomatically. The bottom theories in http://isabelle.in.tum.de/dist/library/HOL/HOL/ are all about classic…

I wonder if the coinductive approach calculus by Pavlovic et al [1, 2] has been considered as a basis for formalisation.

I secretly hope that I will one day get to teach calculus to computer scientists. In that case I would introduce reals as a coinductive data type, and the usual operations (such as differentiation, integration, solving differential equations) as stream operations. That should appeal to programmers, athough it would be weird for conventional mathematicians.

[1] D. Pavlovic, M. Hölzl Escardo, Calculus in coinductive form.

[2] D. Pavlovic, V. Pratt, The continuum as a final coalgebra.

Re: Calculus for mathematicians (1997) [pdf]

#18

Post by jordigh » Thu, May 28, 2015, 11:29 AM UTC

Hm, I always thought Spivak was calculus for mathematicians.

Re: Calculus for mathematicians (1997) [pdf]

#19

Post by tel » Thu, May 28, 2015, 11:40 AM UTC

mafribe wrote: post #17

jojo3000 wrote: post #15

Earlier quoted context omitted.

Even defining the real numbers is already quite involved, for example in Isabelle/HOL it is introduced as quotient over Cauchy sequences: http://isabelle.in.tum.de/dist/library/HOL/HOL/Real.html This is the classical way (and similar to HOL Light or HOL4). AFAIK in Coq the standard way is to introduce the reals axiomatically. The bottom theories in http://isabelle.in.tum.de/dist/library/HOL/HOL/ are all about classic…

I wonder if the coinductive approach calculus by Pavlovic et al [1, 2] has been considered as a basis for formalisation. I secretly hope that I will one day get to teach calculus to computer scientists. In that case I would introduce reals as a coinductive data type, and the usual operations (such as differentiation, integration, solving differential equations) as stream operations. That should appeal to programmers,…

I haven't read the paper, but if you define the reals as constructive Cauchy sequences you'd be forced into a coinnductive definition. Is that equivalent?

Re: Calculus for mathematicians (1997) [pdf]

#20

Post by mafribe » Thu, May 28, 2015, 12:06 PM UTC

tel wrote: post #19

mafribe wrote: post #17

Earlier quoted context omitted.

I wonder if the coinductive approach calculus by Pavlovic et al [1, 2] has been considered as a basis for formalisation. I secretly hope that I will one day get to teach calculus to computer scientists. In that case I would introduce reals as a coinductive data type, and the usual operations (such as differentiation, integration, solving differential equations) as stream operations. That should appeal to programmers,…

I haven't read the paper, but if you define the reals as constructive Cauchy sequences you'd be forced into a coinnductive definition. Is that equivalent?

I'm not familiar with constructive Cauchy sequences. The usual way of using Cauchy sequences is to quotient them by the ideal of Cauchy sequences that converge to 0.