Formal Verification Scientist (Lean 4 & Mathlib)

About The Role What if your deep mathematical training could directly shape how AI systems understand and reason about formal proof? We're looking for Formal Verification Scientists to translate sophisticated human-written mathematics into precise, machine-verifiable Lean 4 formalizations — working at the cutting edge of what proof assistants can express, capture, and automate. This is a fully remote, flexible contract role built for mathematicians who are passionate about formal verification and want their expertise to matter at the frontier of AI research.

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

What You'll Do

• Translate informal mathematical proofs into clean, structured Lean 4 formalizations with an emphasis on clarity, correctness, and reproducibility
• Analyze proofs across domains — algebra, analysis, topology, logic, discrete math — identifying gaps, hidden assumptions, and formalizable sub-structures
• Construct formalizations that test and push the limits of existing proof assistants, particularly where automated tools struggle or fail
• Investigate where and why automated provers break down — whether due to complexity, missing lemmas, or insufficient libraries — and articulate those findings clearly
• Collaborate with AI researchers to design, refine, and evaluate strategies for improving formal verification pipelines
• Develop proof scripts that reveal deeper patterns or generalizations implicit in the original mathematics
• Provide guidance on proof decomposition, lemma selection, and structuring techniques for formal models

Who You Are

• Master's degree or higher in Mathematics, Logic, Theoretical Computer Science, or a closely related field
• Strong foundation in rigorous proof writing and mathematical reasoning across one or more areas: algebra, analysis, topology, logic, or discrete mathematics
• Hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or a comparable proof assistant — Lean 4 strongly preferred
• Deep enthusiasm for formal verification, proof assistants, and the future of mechanized mathematics
• Able to translate dense, informal arguments into well-structured formal proofs that a machine can verify
• Self-directed and comfortable working independently in a remote, async environment

Nice to Have

• Familiarity with type theory, the Curry-Howard correspondence, and proof automation tools
• Experience contributing to or working within large-scale formalization projects such as Mathlib
• Exposure to theorem provers where automated reasoning frequently fails or requires manual scaffolding
• Prior experience with data annotation, evaluation systems, or AI training workflows
• Strong written communication skills for documenting formalization decisions, edge cases, and reasoning strategies

The Ideal Candidate You're a mathematically mature problem-solver who thrives at the intersection of mathematics and computer science. You find genuine satisfaction in taking a dense, elegant human argument and expressing it in a form a machine can understand. You appreciate precision, structural beauty, and the intellectual challenge of resolving gaps that automated tools cannot yet bridge. Why Join Us

• Work directly on cutting-edge AI projects with leading research labs
• Fully remote and flexible — work when and where it suits you
• Freelance autonomy: set your own pace, own your work, collaborate globally
• Gain rare exposure to how frontier AI models are trained and evaluated on formal mathematics
• Meaningful, intellectually stimulating work at the boundary of what proof assistants can do
• Potential for ongoing work and contract extension as new projects launch