Applied Formal Methods Researcher (Lean 4)

About The Role

What if your deep mathematical training could directly shape how AI understands and generates rigorous proofs? We're looking for mathematicians with hands-on formal verification experience to translate complex human arguments into machine-verifiable Lean 4 proofs --- working at the very edge of what automated reasoning can do.

This is a fully remote, flexible contract role for mathematically mature researchers who find beauty in precision and satisfaction in bridging the gap between human intuition and formal logic.

• 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 to surface hidden assumptions, logical gaps, and formalizable sub-structures
• Construct formalizations that stress-test the limits of current proof assistants --- especially where automated tools fall short
• Investigate and articulate why automated provers fail: complexity barriers, missing lemmas, insufficient library coverage, and beyond
• Collaborate with AI researchers to design and refine formal verification pipelines
• Provide expert guidance on proof decomposition, lemma selection, and structuring strategies for formal models
• Develop Lean proofs that reveal deeper generalizations or implicit patterns in existing mathematical arguments

Who You Are

• Holder of a Master's degree or higher in Mathematics, Logic, Theoretical Computer Science, or a closely related field
• Deeply experienced in rigorous proof construction across areas such as algebra, analysis, topology, logic, or discrete mathematics
• Hands-on with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or comparable formal systems --- Lean strongly preferred
• Genuinely passionate about formal verification, proof assistants, and the future of mechanized mathematics
• Able to translate dense, informal mathematical arguments into precise, structured 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, data quality, or AI evaluation workflows
• Strong written communication skills for explaining formalization decisions, edge cases, and proof strategies

Why Join Us

• Work directly on cutting-edge AI research projects alongside leading AI labs
• Fully remote and flexible --- structure your work around your schedule
• Freelance autonomy with intellectually stimulating, high-impact work
• Operate at the frontier of formal mathematics and AI --- mapping the boundary of what machines can reason about
• Potential for ongoing work and contract extension as new projects launch