![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Yesterday I saw a talk by about applications of proof theory to functional analysis by Ulrich Kohlenbach .
As in most technical talks, I didn't understand much from the details, but I find the general idea very attractive: taking a normal proof about a certain structure and using meta-theorems about proof transformations to find proofs of related results on related structures. Many of these proofs would be very hard to find without these methods.
These methods save us from having to do the same work twice (this unnecessary work would be part of the difficulty of finding the new proofs without these methods). It's about using new dynamic tools to guide our suboptimal way of doing mathematics, subject to all our cognitive limitations as human beings. (if it seems like I'm hinting at using computers as theoretical aids for mathematicians, it's because I am (although this talk didn't directly hint at that))
And it's analogous to using abstraction in programming: it saves work by reusing common structures. During the talk, I was thinking of the freedom you get by programming using Lisp. Lisp is a reflective language where you can write self-manipulating code. In Lisp, you can go to any meta-level of abstraction you want: there is no limit.
These sort of proofs may at first seem like an unusual way of doing mathematics, but in fact, we routinely do the same thing at a very simple level: whenever we have a symmetry of variables or similar cases in a proof (I'm thinking of proofs using left vs. right multiplication in group theory), we wave our hands the second time. When we say "it's just like the first one", we are actually unconsciously applying a theorem about proof transformations.
Just like we desire short & elegant computer programs, we desire short elegant proofs in our mathematics. And in that sense, these methods may be analogous to methods of abstraction in programming. The idea is to make life easier by going to whatever meta-level is necessary. Yet, many people seem hesitant to make this jump (either that or they simply have no idea that this would be useful).
I am curious about learning all this type-theory, ML stuff, if only to refine this analogy between programming and mathematics, but unfortunately it seems like the UvA is not the right place for it.
As in most technical talks, I didn't understand much from the details, but I find the general idea very attractive: taking a normal proof about a certain structure and using meta-theorems about proof transformations to find proofs of related results on related structures. Many of these proofs would be very hard to find without these methods.
These methods save us from having to do the same work twice (this unnecessary work would be part of the difficulty of finding the new proofs without these methods). It's about using new dynamic tools to guide our suboptimal way of doing mathematics, subject to all our cognitive limitations as human beings. (if it seems like I'm hinting at using computers as theoretical aids for mathematicians, it's because I am (although this talk didn't directly hint at that))
And it's analogous to using abstraction in programming: it saves work by reusing common structures. During the talk, I was thinking of the freedom you get by programming using Lisp. Lisp is a reflective language where you can write self-manipulating code. In Lisp, you can go to any meta-level of abstraction you want: there is no limit.
These sort of proofs may at first seem like an unusual way of doing mathematics, but in fact, we routinely do the same thing at a very simple level: whenever we have a symmetry of variables or similar cases in a proof (I'm thinking of proofs using left vs. right multiplication in group theory), we wave our hands the second time. When we say "it's just like the first one", we are actually unconsciously applying a theorem about proof transformations.
Just like we desire short & elegant computer programs, we desire short elegant proofs in our mathematics. And in that sense, these methods may be analogous to methods of abstraction in programming. The idea is to make life easier by going to whatever meta-level is necessary. Yet, many people seem hesitant to make this jump (either that or they simply have no idea that this would be useful).
I am curious about learning all this type-theory, ML stuff, if only to refine this analogy between programming and mathematics, but unfortunately it seems like the UvA is not the right place for it.