paid part-time opportunity to formalize math in Lean 4

Stream: general

[Tudor achim]

Hi everyone, I’m Tudor Achim. Together with a small team, we are working on a new AI project and are looking for some help with Lean 4 formalization. If you’re interested in a flexible part-time role formalizing math that wouldn’t meaningfully conflict with continuing open-source contributions to Mathlib, please submit your info in this form and we’ll get back to you! https://docs.google.com/forms/d/e/1FAIpQLSfP04m0PHxoSan8yfnAEKOTylOrbx5VypDg0xZNsjfJ2chWyg/viewform