Mathematical Research Engineer, Mathlib Initiative

Job description

The Mathlib Initiative is hiring Mathematical Research Engineers to lead editorial operations for the world's most ambitious mathematical formalization project. We're building a team to join at a pivotal moment: Mathlib powers projects by Fields Medalists and numerous automated theorem provers (e.g., AlphaProof, Aristotle, Seed-Prover, …), but faces a critical scaling bottleneck that you'll help solve.

The Challenge: 400+ pull requests sit in our review queue. There is an additional backlog of more than 1,000 open pull requests outside the queue. Brilliant contributions from mathematicians worldwide wait weeks for expert review. Increasing review bandwidth is probably the biggest lever for advancing formal mathematics.

Your Mission: Assist with triage and review of incoming contributions. Build and operate the editorial infrastructure that will scale Mathlib from powering individual research projects to supporting an entire ecosystem of mathematical knowledge that AI systems and researchers worldwide depend on.

Role & Responsibilities

Editorial Leadership

  • Triage the review queue: Ensure 90% of pull requests receive expert attention within one week

  • Guide contributors: Provide thoughtful feedback that educates and develops the next generation of Mathlib reviewers

  • Implement standards: Apply established Mathlib quality standards consistently during review

  • Coordinate reviews: Route PRs to appropriate expert reviewers and manage review timelines

Technical Infrastructure

  • Improve automation: Work with engineering team to provide better automated feedback to authors

  • Enhance tooling: Improve the queueboard review dashboard

  • Scale processes: Design systems that work at 100x current contribution volume

  • Mentor reviewers: Recruit and train community members to become expert reviewers

Strategic Impact

  • Enable breakthrough research: Your work directly unlocks formalization of major theorems and AI research

  • Build the ecosystem: Help downstream projects integrate seamlessly with Mathlib

  • Shape the future: Participate in decisions that will define how mathematics evolves

You Should Apply If

Required Qualifications

  • Active Mathlib contributor with substantial merged contributions

  • Experienced reviewer who understands Mathlib's design principles and quality standards

  • Mathematical expertise at research level (PhD preferred, exceptional cases considered)

  • Technical judgment for making architectural decisions in large mathematical libraries

Ideal Candidate

  • Editorial mindset: You see the big picture and can balance perfectionism with pragmatic progress

  • Communication skills: You can guide contributors constructively while maintaining high standards

  • Systematic thinking: You naturally think about processes, bottlenecks, and scaling challenges

  • Community focus: You care about building an inclusive, supportive environment for contributors

Why This Role Matters

  • For Mathematics: You're building the infrastructure for a new era where mathematical knowledge is machine-verifiable, searchable, and universally accessible.

  • For AI: Your work creates the training ground where the next generation of reasoning systems learn to do mathematics.

  • For Your Career: This is a unique opportunity to shape an entirely new field at the intersection of mathematics, computer science, and AI—while working with some of the most brilliant mathematical minds of our time.

  • For Science: Formal mathematics will transform scientific computing, software verification, and critical infrastructure. You're laying that foundation.

Position Details

Work Structure

  • Minimum 1 day per week as an independent contractor; 2 days preferred

  • Full-day commitment: We want focused, dedicated days, not scattered hours

  • Flexible scheduling: Work the days that fit your research/teaching schedule

  • Fully remote: Work from anywhere with reliable internet

Compensation: $320-$640 daily rate based on seniority and experience

Team & Culture

  • Growing the Initiative: Help build the Mathlib Initiative team culture and practices

  • Collaborative integration: Work closely with existing Mathlib maintainers and reviewers, and community processes

  • Research-friendly: Designed to work well alongside academic positions and research commitments

High impact Every day of work directly advances the entire formal mathematics ecosystem

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 current Mathlib contributors who want to help solve the scaling challenges they see every day, while building something genuinely transformational.

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

  • Your Mathlib contributions and reviewing experience

  • Your vision for scaling mathematical formalization

  • How this role fits with your other commitments

Informal inquiries may be made to <johan@renphil.org>, using “Title - Application Mathematical Research 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.