Introduction: Pierpaolo Frasa

Stream: new members

[Tainnor]

Since I've been asking a number of questions recently (thanks to everyone who was kind enough to help - I would have given up without all the help), I thought it might be a good idea to introduce myself.

My name is Pierpaolo Frasa and I live in Berlin. In contrast to most (?) people here, I'm not a professional mathematician, only a "hobbyist". I'm a software developer but I've also been fascinated by mathematics for many years now. I'm currently enrolled in a MSc in mathematics at a remote university, but I have absolutely no rush to complete the degree any time soon - so that leaves enough time for exploration (I did my BSc in mathematics in much the same way). I'm mostly fascinated by anything that is related to logic and computation. - unfortunately, my university doesn't offer almost any courses in that department (I wrote my thesis about cryptography which is also an area that I enjoy).

After playing a bit with Coq in the past, I more recently picked up Lean, worked through quite a bit of "mathematics in Lean" (currently I'm in the topology chapter) and I'm also working on formalising parts of my course notes for Complex Analysis which gives me more of a "hands-on" experience. My biggest "success" so far has been formalising the uniqueness of C as a 2-d extension of R (it's actually the unique finite-dimensional extension, but that requires heavier machinery to prove) and currently I'm trying to set up the topological and metric space structure of C. I'm still struggling with a lot of things (mainly finding the right theorems in mathlib, and sometimes mathlib operates at a level of abstraction that is just currently a bit too high for me), but I'm making progress.

[Tainnor]

If someone is curious, I put my code for the complex analysis stuff here: https://gitlab.com/pfrasa/complex.lean/ - it's probably terribly unidiomatic etc., though.

Also, what's the policy for getting write access to mathlib? I'm obviously nowhere near being able to contribute anything of substantial value, but I did spot a couple of typos here and there (e.g. "Weierstrass" is misspelt).

[Kim Morrison]

@Tainnor, you get write access by asking for it. I would do it now, except I'm not sure of your github user name.

[Kevin Buzzard]

And PRs fixing spellings are most definitely welcome!

[Kevin Buzzard]

And we need the Weierstrass P-function (or equivalent) for FLT!

[Tainnor]

My Github handle is Fryie

[Kim Morrison]

@Tainnor, invitation sent!