Kevin Allen: Introduction

Stream: new members

[Kevin Allen]

Hi everyone. My name is Kevin Allen and I am an MSc Maths student in University College Dublin (soon to be PhD student). I have recently been looking into Lean out of curiosity after watching a couple of Kevin Buzzard's videos on youtube, and I completed the Natural Number Game and the further Maths Challenges on the github page.
I am currently doing my MSc project on topics in finite geometry (projective planes, semifields etc.) and was thinking I could introduce some Lean to help learn Lean and the project material. I had a look through the library and couldn't find a definition of a projective plane so that could possibly be a start for me. Would anyone have advice for how to get started? Much appreciated!

[Bryan Gin-ge Chen]

There are some old threads related to axiomatic geometry linked here; see also @Vaibhav Karve's work on axiomatic geometry in Lean.

[Adam Topaz]

I also have a branch where I started some sketches about projective geometry (with the eventual goal of proving the fundamental theorem of projective geometry), but I haven't had the time nor energy to work on it for a while... I think it's branch#proj-space-quot ?

(This has nothing about the axiomatic approach though)

[Kevin Allen]

Brilliant. Thanks for the resources. I am still quite new to github so I will have some fun figuring that out too

[Bryan Gin-ge Chen]

We have a page for new mathlib contributors, but also feel free to ask any questions about git or github here!