Lean Engineer
Resolution is an independent nonprofit AI-alignment research institute that combines theory, empirics, and research automation to pursue higher confidence in aligned advanced AI.
About Resolution
Resolution conducts AI-alignment research, with work spanning scalable oversight, learning theory, agent foundations, interpretability-related research, and automation. It was formed from Timaeus Research and researchers from the UK AISI Alignment Team, with a major in-person presence in Berkeley.
Skills
Candidate Availability
Required and preferred rules are kept separate and reflect the wording in the original posting.
About the Role
You will establish conventions, architecture, and review practices that make Lean and AI-assisted autoformalization reliable at scale. You will maintain shared formalization infrastructure, improve Lean projects, and help researchers develop tools and workflows without needing to manually review every proof.
Requirements
- Several years of experience writing Lean and mathlib
- Expertise in Lean community practices
- Experience as an AI power user with autoformalization
- Strong mathematics or theoretical computer science background
- Relevant bachelor's degree minimum
- Clear communication skills
- Willingness to work closely with researchers and engineers
Responsibilities
- Nurture Lean expertise throughout the organization and champion Lean and autoformalization
- Build and maintain proof harnesses, code-review workflows, and other structures for trusting agent autoformalization outputs
- Build and maintain shared Lean libraries with clear definitions, useful abstractions, and structures that support review and automated research
- Consolidate overlapping formalizations, resolve inconsistent definitions, and create shared reusable foundations
- Improve the reliability, maintainability, and performance of shared Lean projects
- Support researchers in developing custom tools, tactics, and workflows
Benefits
- Five weeks of paid vacation plus public holidays
- Comprehensive medical, dental, and vision insurance
- Unlimited sick leave
- Unconditional 401(k) contribution equal to 4% of salary
- Visa sponsorship for relocation to Berkeley
Hiring Process
Application review → screening call (30 minutes) → experience interview (1 hour) → optional live technical/work test → individual conversations with Geoffrey and other team members (30 minutes each).