Metaprogrammer, Mathlib Initiative

Design and implement Lean metaprograms—tactics, linters, and code actions—to accelerate mathematical formalization in Mathlib.
- Create new tactics and linters that enable higher-level abstraction and faster proof development in Mathlib.
- Maintain existing metaprograms, review specialist pull requests, and support the Mathlib community.
- Proficiency in Lean metaprogramming and computational methods (linear algebra, polynomials, interval arithmetic) required.
- Open-source and Mathlib contribution experience strongly desired.
- Full-time remote position; two-year fixed-term contract.

Design and implement Lean metaprograms—tactics, linters, and code actions—to accelerate mathematical formalization in Mathlib.
- Create new tactics and linters that enable higher-level abstraction and faster proof development in Mathlib.
- Maintain existing metaprograms, review specialist pull requests, and support the Mathlib community.
- Proficiency in Lean metaprogramming and computational methods (linear algebra, polynomials, interval arithmetic) required.
- Open-source and Mathlib contribution experience strongly desired.
- Full-time remote position; two-year fixed-term contract.

Renaissance Philanthropy is a nonprofit that aims to increase the ambition of philanthropists, scientists, and innovators by advising philanthropists, surfacing breakthrough ideas, and incubating ambitious initiatives.