Lean Proof Contractor

Core responsibilities:

• Write proofs in Lean for mathematical AI safety research
• Convert published papers' theorem statements and proofs into Lean
• Transform the team's conjectures into Lean propositions and prove or disprove them
• Teach team members how to use Lean to improve mathematical conjecturing feedback loops
• Build and maintain Mathlib extensions while upholding best practices and conventions

This role contributes to AI safety research by formalizing mathematical proofs, helping to ensure the reliability and correctness of AI systems through rigorous mathematical verification.

Required skills and qualifications:

• Experience writing proofs in Lean
• Strong mathematical background
• Ability to convert mathematical papers into formal proofs
• Teaching and knowledge transfer skills
• Experience with Mathlib extensions and best practices

No compensation, perks, or culture highlights mentioned in the posting.

Dovetail appears to be an organization focused on AI safety research, specifically using formal verification methods like Lean to ensure mathematical correctness in AI systems.