Hi from Mike George

Stream: new members

[Michael George]

Hello,

I'm a CS PhD with interests in PL, FV, and various topics in math. I've made a few small contributions to coq's math-classes library, and I'm just starting to learn lean in my free time.

I'm hoping eventually to write some computational geometry algorithms (e.g. polygon intersection / union), but I think I will start small by implementing a priority queue. AFAICT these are not currently implemented in mathlib, so maybe this would be a good thing to eventually contribute? If so, does it make sense for me to make a fork and work there for now? Also, should I be using lean 3 or lean 4?

Thanks, and looking forward to learning more!

[Alex J. Best]

Hi! Probably using Lean 4 will suit you better for more programmy things, its still under development of course and the maths library isn't fully ported yet, but certainly advanced enough for implementing data structures. I just had a quick search and found docs4#Std.BinomialHeap already, maybe that can be some inspiration or you want to build on top of this instead of starting from scratch.
Generally people contributing to mathlib or mathlib4 or std4 ask the maintainers for push access to the (non-master branches) of that repo rather than using a fork.