Applied Formal Methods Researcher (Lean 4)

About The Role What if your deep mathematical training could directly shape how AI understands and constructs formal proofs? We're looking for mathematicians with hands-on experience in formal verification to work at one of the most exciting intersections in modern AI research — mechanized mathematics. You'll translate rigorous human-written arguments into machine-verifiable Lean 4 proofs, explore the boundaries of what automated provers can and cannot do, and help build the datasets that train the next generation of AI reasoning systems. This is a fully remote, flexible contract role designed for mathematicians who love precision, structure, and the intellectual challenge of formal verification.

• 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 correctness and readability
• Analyze proofs across domains — identifying hidden assumptions, logical gaps, and formalizable sub-structures
• Construct formalizations that probe and test the limits of existing proof assistants, particularly where automation breaks down
• Investigate why automated provers fail on specific problems — whether due to complexity, missing lemmas, or insufficient libraries — and document your findings clearly
• Collaborate with AI researchers to refine strategies for improving formal verification pipelines
• Provide expert guidance on proof decomposition, lemma selection, and structuring techniques for formal models
• Develop highly reproducible proof scripts aligned with mathematical best practices and Lean idioms
• Create Lean proofs that expose deeper patterns or generalizations implicit in the original mathematics

Who You Are

• Holder of a Master's degree or higher in Mathematics, Logic, Theoretical Computer Science, or a closely related field
• Strong foundation in rigorous proof writing across areas such as algebra, analysis, topology, logic, or discrete mathematics
• Hands-on experience with Lean (Lean 3 or Lean 4), with Lean 4 strongly preferred — experience with Coq, Isabelle/HOL, or Agda also considered
• Deep enthusiasm for formal verification, proof assistants, and the future of mechanized mathematics
• Able to translate dense, informal mathematical arguments into precise, machine-checkable formal proofs
• Self-directed and comfortable working independently in an asynchronous, remote environment

Nice to Have

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

The Ideal Candidate You're a mathematically mature problem-solver who thrives at the frontier of formal verification. You find genuine satisfaction in taking a dense, elegant human argument and expressing it in a form a machine can verify. You appreciate precision and structural beauty — and you're energized by the challenge of resolving gaps that automated tools cannot yet bridge. Why Join Us

• Work directly on cutting-edge AI research projects alongside leading AI labs
• Fully remote and flexible — work when and where it suits you
• Freelance autonomy: set your own pace within a 10–40 hour weekly range
• Gain rare exposure to how advanced AI reasoning systems are built and trained
• Contribute to research that is actively pushing the frontier of what machines can prove
• Potential for ongoing work and contract extension as new projects launch