Formal Verification Scientist (Lean 4 & Mathlib)

About The Role

What if your mathematical expertise could directly shape how AI understands and reasons about formal proof? We're looking for mathematicians and logicians with hands-on experience in formal proof systems — particularly Lean 4 and Mathlib — to help translate complex mathematical arguments into precise, machine-verifiable formalizations.

This is a fully remote, flexible contract role working at the cutting edge of AI research and formal verification. You'll be tackling problems that sit beyond the reach of automated provers — doing work that genuinely maps the frontier of what machines can verify and understand.

• Organization: Alignerr
• Type: Hourly Contract
• Location: Remote
• Commitment: 10–40 hours/week
  
  

What You'll Do

• Translate informal mathematical proofs into Lean 4 and related proof systems with an emphasis on clarity, correctness, and reproducibility
• Analyze both general and domain-specific proofs to identify gaps, hidden assumptions, and formalizable structure
• Construct formalizations that push the current limits of proof assistants
• Investigate where automated provers break down — and why — to help improve formal verification pipelines
• Write clean, readable, well-structured proof scripts that expose deeper mathematical structure
• Advise on proof decomposition, lemma selection, and formal architecture
• Collaborate with AI researchers to advance high-integrity dataset creation and model reasoning
  
  

Who You Are

• Holds a Master's degree or higher in Mathematics, Logic, Theoretical Computer Science, or a related field
• Deeply comfortable with rigorous proof writing across algebra, analysis, topology, logic, or discrete mathematics
• Has hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or similar formal proof systems — Lean 4 strongly preferred
• Excited by formal verification and the challenge of expressing human mathematical arguments in forms machines can check
• Able to work independently, manage ambiguity, and produce high-quality output without close supervision
  
  

Nice to Have

• Experience with Mathlib or other large-scale formalization projects
• Familiarity with type theory, the Curry–Howard correspondence, and proof automation tools
• Experience working in domains where automated provers fail and require manual scaffolding
• Strong communication skills for documenting and explaining formalization decisions and edge cases
  
  

Sample Tasks

• Formalize classical theorems and compare machine-verifiable proof structures against textbook arguments
• Identify and document where proof automation breaks down and construct manual scaffolding to fill gaps
• Build Lean proofs that reveal hidden structure, generalizations, or alternative formalization paths
  
  

Why Join Us

• Work on frontier AI research with leading AI labs — your output directly improves how models reason about mathematics
• Fully remote and async — work when and where it suits you
• High autonomy and flexible freelance structure that respects your time
• Collaborate with a network of top mathematicians, logicians, and computer scientists
• Potential for ongoing contract extension as new projects launch