David Kinkead

Stream: new members

[David Kinkead]

Hi all,

Just introducing myself as suggested in the channel description.

I'm David, based in London, and I'm in the final year of a Maths BSc (well, final two years because part-time). Areas of greatest interest to me so far are number theory and category theory. And Lean, obviously.

I stumbled across Lean some time ago while listening to Kevin Buzzard on an old "Joy of Why" podcast. One very steep learning curve later, I'm now completely hooked.

To get myself properly up to speed, and hopefully in a position to contribute to mathlib some day, I've been working my way through Lawvere & Schanuel's Conceptual Mathematics, coding up the definitions, theorems, and exercises in Lean as I go. I'm a little over half way through. In case anyone's interested, the codebase can be found at https://github.com/davidkinkead/conceptual_mathematics with the Verso output hosted at https://davidkinkead.github.io/conceptual_mathematics

Looking forward to learning from everyone here. Zulip seems like an amazing resource!

[David Renshaw]

It's cool to see Verso being used like this!

[David Kinkead]

Verso's great! I've really enjoyed working with it.

[suhr]

By the way, since you are interested in category theory, you might find this interesting as well: https://mikeshulman.github.io/catlog/catlog.pdf

[Kevin Buzzard]

You should come to Xena on Thursday 5-8pm at Imperial (last one of the year is a week today) if you're in London.

[David Kinkead]

Thanks - I won't be able to make the one next week, I'm afraid, but I'd love to come along if you're running Xena again in the new year?

[Kevin Buzzard]

It runs during Imperial's term dates (which you can Google)