DevOps Engineer, Mathlib Initiative

Job description

The Mathlib Initiative is hiring a DevOps Engineer to solve cutting-edge distributed systems challenges that will transform how mathematics is done worldwide. You'll be pioneering technical innovation in a greenfield domain—applying modern DevOps practices to formal mathematics infrastructure. Your work will enable open source impact at global scale.

The Challenge: The Mathlib ecosystem is expanding from a single foundational library to dozens of specialized mathematical libraries, with Mathlib as their foundation. This transformation requires sophisticated infrastructure for automated dependency management, cross-repository testing, and seamless integration across all downstream projects—all while maintaining the rigorous standards that make formal mathematics possible.

Your Mission: Design and build the backbone infrastructure to scale mathematical formalization. Your work will power individual research projects and support an ecosystem of mathematical knowledge, upon which AI systems and researchers worldwide will depend.

Role & Responsibilities

Infrastructure Architecture

  • Multi-repository ecosystem: Build tooling to manage dependencies across specialized mathematical libraries

    Automated testing pipelines: Design cross-repository CI/CD that validates changes across the entire ecosystem

    Integration platforms: Connect with Reservoir (Lean's global project repository) and other ecosystem tools

Automation & Tooling

  • Dependency management: Enhance and maintain automated upgrade systems for downstream libraries

  • Patch automation: Build tooling to automatically apply patches and syntactic transformations during updates

  • GitHub Actions: Develop sophisticated workflows for mathematical verification

  • Monitoring & alerts: Implement systems to track ecosystem health and performance

Collaboration & Integration

  • Cross-team collaboration: Work closely with the Lean FRO language development team and Mathlib maintainer team on infrastructure integration

  • Community support: Provide technical guidance to downstream project maintainers

  • Documentation: Create clear guides for projects adopting the infrastructure

Key Qualifications

  • DevOps expertise with experience in CI/CD, automated testing, and infrastructure management

  • GitHub Actions proficiency and experience with complex workflow automation

  • Distributed systems thinking for managing dependencies across multiple repositories

  • Strong communication skills for collaborating with both technical and mathematical domain experts

Ideal Candidate

  • Open source experience contributing to or maintaining infrastructure for large software projects

  • API integration experience, particularly with GitHub and the chat platform Zulip

  • Problem-solving mindset for tackling novel infrastructure challenges

  • Mission alignment with advancing mathematical formalization and open science

Nice to Have

  • Experience with formal verification tools or academic software infrastructure

  • Knowledge of package management systems and dependency resolution

  • Background in build systems for complex software projects

Why This Role Matters

  • For Mathematics: You're building the infrastructure that will make mathematical knowledge machine-verifiable, searchable, and universally accessible—transforming how mathematics research and education happen.

  • For Your Career: This is a unique opportunity to pioneer DevOps practices in formal mathematics, working on technically challenging problems that don't exist anywhere else in the software industry.

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

  • For Innovation: You'll be applying cutting-edge DevOps practices to an entirely new domain, creating solutions from which the broader software community will learn.

Position Details

  • Work structure

    • Full-time position: Employee of Renaissance Philanthropy

    • Fully remote: Work from anywhere with reliable internet, with teammates in North America and Europe

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

  • Compensation: $80k – $120k based on experience + benefits

  • Team & Culture

    • Collaborative environment: Coordinate with the Lean FRO team and mathematical domain experts on infrastructure integration

    • Mission-driven: Join a team passionate about transforming mathematical practice

    • Technical excellence: 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

This position is perfect for DevOps engineers who want to apply their infrastructure expertise to genuinely transformational work that will impact mathematics, AI research, and scientific computing worldwide.

To apply, use the application link to send us your CV and a brief cover letter explaining:

  • Your DevOps and infrastructure automation experience

  • Why you're excited about building infrastructure for mathematical software

  • Examples of complex CI/CD or multi-repository systems you've designed


Informal inquiries may be made to <johan@renphil.org>, using “Title - Application DevOps Engineer” as the subject. Applications should be submitted here by Sunday, September 14, 2025

About The Mathlib Initiative
The Mathlib Initiative is a new 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.