Mathlib Initiative, Metaprogrammer

The Mathlib Initiative is hiring a Lean Metaprogrammer to assist with the development of Lean’s mathematics library Mathlib. Mathlib already relies heavily on a valuable set of metaprograms in the form of tactics, linters, decorators such as to_additive, to_dual, code actions, and more. You will assist in maintaining what we have and especially in creating many more such tools.


The Challenge: As Mathlib grows, so does its dependence on metaprogramming. Custom tactics allow formalisers to work at higher levels of abstraction, and so speed up the formalisation process. Better tactics also result in more maintainable and more understandable proof scripts. Linters enforce code quality and can provide real-time feedback to aid education. Code actions significantly improve the ergonomics of development. Such tools are also force multipliers: a tool written by a single person may benefit an arbitrary number of users. We need more of these.

About The Mathlib Initiative

The Mathlib Initiative is a programme of Renaissance Philanthropy, created to support the ongoing digitization of mathematics. The Initiative directly supports the maintenance, growth, and development of Lean’s library of formal mathematics known as mathlib. It also supports related repositories in the Lean ecosystem. Mathlib is a massively-collaborative, open-source library of mathematics written using the Lean proof assistant.

All people hired by the Mathlib Initiative will be employed by Renaissance Philanthropy.

About Renaissance Philanthropy

Renaissance Philanthropy is a nonprofit organization that fuels a 21st-century renaissance by increasing the ambition of philanthropists, scientists and innovators. In the first year, Renaissance Philanthropy catalyzed more than $214M in philanthropic funding for science, technology, and innovation, launching 10+ initiatives across AI, education, climate, health, and scientific infrastructure. The organization designs time-bound, thesis-driven funds led by field experts and inspires talent to take action through playbooks and communities. From accelerating mathematical discovery to expanding talent mobility, Renaissance Philanthropy is building the connective tissue between exceptional ideas and resources to create breakthroughs that transform entire fields.

What You'll Do

In this role, you will: 

  • Design and implement key Lean metaprograms to support the growth and maintenance of Mathlib.

  • Ship fast, maintainable, tested code and so speed up its development.

  • Suggest and implement ideas for impactful applications of metaprogramming in Mathlib.

  • Contribute your work to the relevant repository (usually Mathlib) using GitHub pull requests.

  • Engage with review of your work, provided either by members of the Mathlib Initiative team, or by wider members of the Lean community, especially members of the Mathlib Maintainer team.

Your primary responsibility will be to identify, implement, and support the development of:

  • new tactics

  • new linters

  • new code actions

Secondary responsibilities will include the maintenance of Mathlib’s existing metaprogramming and the support of incoming metaprogramming contributions. This work is likely to include:

  • Identifying locations in Mathlib where any new tactics you create should be used.

  • Assisting with the roll out of new linters, refactoring Mathlib as needed.

  • Reviewing pull requests which require specialist metaprogramming expertise

  • Addressing issues which arise in existing metaprograms (e.g., a bug or performance issue in a tactic or linter)

  • Collaborate with and provide assistance to members of the Mathlib Initiative as needs for your particular expertise arise.

You Should Apply If

Required Qualifications:

  • Lean Metaprogramming Expertise: This role requires someone who is already proficient in Lean and especially in Lean metaprogramming.

  • Strong communication skills: This role will require frequent collaboration with both technical and mathematical domain experts.

  • Mission alignment: We seek people who care about advancing mathematical formalization and open science.

Ideal Candidate:

  • Open source experience: Experience contributing to open-source projects is desirable.

  • Mathlib contributor: Experience contributing to Mathlib is desirable.

Why This Role Matters

  • For Mathematics: You will build tools that make mathematical knowledge machine-verifiable, searchable, and universally accessible—transforming how mathematics research and education take place.

  • For Your Career: This is a unique opportunity to build powerful tools which will manipulate mathematics digitally and at scale.

  • For Global Impact: Your work will enable mathematical breakthroughs worldwide, supporting everything from solo mathematicians to AI research labs to university classrooms to critical software verification.

Position Details

Work Structure:

  • Full-time position: You will be a full-time employee.

  • Fully remote: You may work from anywhere with reliable internet; your teammates are currently based in Europe and North America.

  • Flexible schedule: Focus on results and collaboration across time zones.

Compensation:

  • $100K - $160K (based on experience and location) + benefits

  • Growth opportunity: As Mathlib scales, so does the importance of all force-multiplier roles such as this one. We understand career development is important.

Team & Culture

  • Collaborative environment: You will join a highly collaborative team supporting a hugely collaborative open-source project.

  • Mission-driven: You will join a team that is passionate about transforming mathematical practice.

  • Technical excellence: We have high standards for code quality and system reliability.

Diversity

We encourage anyone who is interested in this role to apply, regardless of whether you feel you meet 100% of the qualifications. The top candidates will bring their own unique perspectives, experiences, and backgrounds from a variety of industries along with many but not necessarily all the skills listed above.

Recruiting, hiring, mentoring, and retaining a diverse workforce is critical to our success. All qualified applicants will receive consideration for employment without regard to race, colour, religion, sex, sexual orientation, gender identity, national origin, disability, or status as a protected veteran. 

Renaissance Philanthropy is an equal-opportunity employer. We celebrate diversity and are committed to creating an inclusive environment for all employees.

Next Steps

Apply here.

Informal inquiries may be made to <hiring@mathlib-initiative.org>, using “Title - Metaprogrammer” as the subject