Tjeerd Jan heeringa

Stream: new members

[Tjeerd Jan Heeringa]

Hi Everyone,

I'm Tjeerd Jan Heeringa, an applied mathematician from the Netherlands. I study the mathematical foundation of machine learning. I work on describing the natural function spaces for neural networks. These turn out to be reproducing kernel Banach spaces, which the majority of my research is about.

I have heard about lean a couple of times before, and now with my PhD at the University of Twente nearing its end, I wanted to try it out. I did some tutorials and then decided to implement the reproducing kernel theory in Lean. You may have seen some of my questions about that. So far, formalizing mathematics in lean has been very satisfying. I would be happy if I could work in/on this as (a part of) a PostDoc.

My implementation of kernel theory in Lean is almost containing all the results I know about the real-valued reproducing kernel Hilbert spaces (RKHS). Whilst it is not the latest and greatest involving complex-valued and vector-valued RKHS, it includes the parts taught in functional analysis courses. I didn't see anything in lean 4 (there was an unmerged pull-request in lean 3) about RKHSs, so I was planning on making a pull-request for the real-valued stuff, and expand in it on a different pull-request. The current one would be 1500 lines already :sweat_smile: