Principal Research Software Engineer

About the Lean Focused Research Organization (FRO):

The Lean Focused Research Organization (FRO) is committed to revolutionizing how Lean, a proof assistant and programming language, is utilized across various sectors. We aim to make Lean a cornerstone in formal mathematics, software and hardware verification, software development, AI in mathematics and code synthesis, and new educational methodologies in math and computer science. Our goal is to cultivate a dynamic, decentralized ecosystem that thrives on diversity and collaboration, engages with a global community, and fosters open-source contributions. 

We are seeking a talented and motivated Principal Research Software Engineer to join our team at the Lean FRO. As a Principal Research Software Engineer, you will play a crucial role in developing and enhancing Lean, collaborating with leading mathematicians and computer scientists worldwide, and contributing to the FRO’s long-term sustainability and success. You will have the opportunity to contribute to groundbreaking research, create innovative solutions, and shape the future of formal verification.

• Develop and lead efforts to improve Lean, including proof automation, standard libraries, and overall ecosystem.
• Engage with external researchers interested in Lean to help resolve their issues and identify improvements for long-term success with Lean.
• Collaborate with people across the Lean FRO to help set strategic and short-term priorities and uphold a consistently exceptional quality bar for usability, scalability, and simplicity.
• Solve hard scalability problems that arise as the Lean ecosystem grows in size and complexity.
• Optimize Lean's performance and scalability for efficient theorem proving.
• Conduct code reviews, provide constructive feedback, and maintain code quality standards.
• Stay up to date with the latest advancements in formal methods and theorem proving techniques.
• Actively engage in the open-source community; understand key trends and proactively recommend solutions, identify user needs, respond to feedback, and address bug reports. 
• Act as an ambassador for Lean FRO. This may include presenting talks, participating in academic conferences or workshops, contributing to papers and articles, and other activities that promote Lean’s continuous improvement and growth.

• Bachelor's, master's, or Ph.D. in Computer Science, Mathematics, or a related field. 
• Strong functional programming skills (experience in Lean is a big plus).
• Familiarity with formal methods, interactive theorem provers, or related areas.
• Experience with software development practices such as version control, code testing, and debugging.
• Excellent problem-solving skills and ability to think critically.
• Strong written and verbal communication skills.
• Self-motivated and able to work both independently and in a team environment.
• Passion for mathematics, formal methods, and the advancement of scientific research.
• Through actions, interactions, and communications with others, demonstrate a commitment to diversity, inclusion, and cultural awareness.

• Experience contributing to open-source projects.
• Knowledge of mathematical logic, type theory, or related areas.
• Familiarity with other interactive theorem provers such as Coq, Isabelle, or Agda.
• Background in mathematical research or proof theory.

• A competitive salary and comprehensive benefits package.
• An opportunity to change the world and work with some of the smartest and most talented experts from different fields.
• Excellent medical, dental, and vision insurance through a PPO plan; parental leave.
• Generous time off and paid holidays.
• Wellness allowance for fitness and wellness activities.

We aim to help fill a structural gap in today's R&D system. We enable fundamental research that requires unusual levels of scale and coordination yet is not rapidly monetizable by industry. We’re bringing together top talent from academia, industry, and startups to build a new model for innovative R&D. As an incubator within the Schmidt Futures Network, we identify high-impact scientific or technical research and development opportunities, ultimately defining and launching these projects as Focused Research Organizations.

We are an Equal Employment Opportunity employer that proudly pursues and hires a diverse workforce. We do not make hiring or employment decisions on the basis of race, color, religion or religious belief, ethnic or national origin, nationality, sex, gender, gender-identity, sexual orientation, disability, age, military or veteran status, or any other characteristic protected by applicable local, state, or federal law or company policy. We strive for a healthy and safe workplace and strictly prohibit harassment of any kind.

Tags