I don't have a lot of reach on here, so boosts would be greatly appreciated. I'm looking for someone to join my team at the Lean FRO as a metaprogrammer with a view towards library quality. I'm working toward a future in which ITPs are a joy to use productively for mathematics and software verification. I believe that to get there, we need to get a lot better at building libraries that are complete, consistent and scalable, and a key factor in that will be to have excellent tooling for monitoring and improving the quality of our libraries. At the Lean FRO, we are building such tools. This includes our linting framework and many elaborator features, but it also extends to more advanced tools, such as our work-in-progress library QA management tool Grove, which I talked about at EuroProofNet last year. And we have many more ideas (and you might as well!). If you are interested in helping make Lean a better tool for building high-quality proof developments, please message me! Ideally, you have experience with Lean metaprogramming or building other PL-related tooling, and/or have thought a lot about how to build high-quality proof libraries in an ITP (doesn't have to be Lean). This is a fully remote, full-time or part-time position. The Lean FRO is able to hire people from most places in the world. Link to my (slightly outdated) EuroProofNet talk: https://youtu.be/qb9kN6ligY4 #FediHire #GetFediHired