Formal Methods (Lean 4) Expert at Mercor

Formal Methods Expert (Lean 4) | $95/hr | Worldwide Remote

Mercor is partnering with a leading AI research lab to enhance expert-level reasoning in frontier AI models. We are seeking experienced formal methods specialists to design rigorous theorem-proving problems, review peer-authored content, and evaluate AI-generated proofs for correctness and mathematical rigor.

What You'll Do

• Design expert-level problems spanning theorem proving, program verification, and formalization of mathematics
• Review peer-authored problems for clarity, genuine difficulty, and ground-truth correctness
• Evaluate and compare AI model outputs — including proofs, tactics, and formalizations — delivering Accept / Revise / Reject verdicts with detailed written rationale

Ideal Qualifications

• Strong background in formal verification and interactive theorem proving
• Hands-on experience with Lean 4 (and mathlib), Coq, Isabelle, or Agda
• Solid understanding of type theory, mathematical logic, and program verification
• Excellent technical writing skills and meticulous attention to detail

This is a flexible, remote contractor role ideal for researchers, academics, or engineers with deep expertise in formal methods who want to contribute to cutting-edge AI development.